Issues

• Version number in build artifacts

  LS-Lab/KeYmaeraX-release#114 · Filter by author wadoon opened on Jan 10, 2025
  3

• Unable to use built-in implicitly defined functions (e.g., sin(x))

  LS-Lab/KeYmaeraX-release#113 · Filter by author wdsmth opened on Jan 29, 2024
  1

• Error with derived axioms database in KeYmaera 5.0.2

  LS-Lab/KeYmaeraX-release#112 · Filter by author ytzemih opened on Dec 14, 2023
  2

• Input {48, MemoryConstrained[...]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]}

  LS-Lab/KeYmaeraX-release#109 · Filter by author krooken opened on Aug 23, 2023
  2

• [UI] [enhancement] Not obvious to user why diRule breaks tactic editor goal-switching

  LS-Lab/KeYmaeraX-release#98 · Filter by author rbohrer opened on Jan 13, 2022
  6

• Late definition usubst clash checking leads to less direct error messages

  LS-Lab/KeYmaeraX-release#96 · Filter by author rbohrer opened on Jan 13, 2022

• [Enhancement request] useLemma with USubst or unification from Web UI

  enhancementUI
  LS-Lab/KeYmaeraX-release#82 · Filter by author rbohrer opened on Jun 10, 2021

• Tactic serialization of "pending" generates tactic that doesn't parse due to string escaping

  bugUI
  LS-Lab/KeYmaeraX-release#79 · Filter by author rbohrer opened on Jun 3, 2021

• Proof won't rerun lemmas unless lemmadb cleared and prover restarted by hand

  LS-Lab/KeYmaeraX-release#77 · Filter by author rbohrer opened on May 31, 2021

• Cryptic error when using comma-separated declaration syntax in SharedDefinitions

  LS-Lab/KeYmaeraX-release#76 · Filter by author rbohrer opened on May 19, 2021

• Is there any plan to make user-defined tactics usable on the UI?

  UI
  LS-Lab/KeYmaeraX-release#75 · Filter by author rbohrer opened on May 13, 2021

• Vector and Matrix Support

  enhancement
  LS-Lab/KeYmaeraX-release#69 · Filter by author zstone1 opened on Sep 24, 2020
  5

• Scala 2.13/dotty compatibility

  wontfix
  LS-Lab/KeYmaeraX-release#68 · Filter by author zstone1 opened on Jun 8, 2020
  5

• Errors when referencing a subtactic within another subtactic

  LS-Lab/KeYmaeraX-release#60 · Filter by author EphesosX opened on Sep 4, 2019
  1

• QE fails when combining quantifiers and function symbols.

  enhancement
  LS-Lab/KeYmaeraX-release#43 · Filter by author nrfulton opened on Sep 27, 2017