All issues

搜索 results

Version number in build artifacts

Status: Open.

#114 In LS-Lab/KeYmaeraX-release;

· wadoon opened on Jan 10, 2025

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

Status: Open.

#113 In LS-Lab/KeYmaeraX-release;

· wdsmth opened on Jan 29, 2024

Error with derived axioms database in KeYmaera 5.0.2

Status: Open.

#112 In LS-Lab/KeYmaeraX-release;

· ytzemih opened on Dec 14, 2023

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

Status: Open.

#109 In LS-Lab/KeYmaeraX-release;

· krooken opened on Aug 23, 2023

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

Status: Open.

#98 In LS-Lab/KeYmaeraX-release;

· rbohrer opened on Jan 13, 2022

Late definition usubst clash checking leads to less direct error messages

Status: Open.

#96 In LS-Lab/KeYmaeraX-release;

· rbohrer opened on Jan 13, 2022

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

enhancement

UI

Status: Open.

#82 In LS-Lab/KeYmaeraX-release;

· rbohrer opened on Jun 10, 2021

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

bug

UI

Status: Open.

#79 In LS-Lab/KeYmaeraX-release;

· rbohrer opened on Jun 3, 2021

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

Status: Open.

#77 In LS-Lab/KeYmaeraX-release;

· rbohrer opened on May 31, 2021

Cryptic error when using comma-separated declaration syntax in SharedDefinitions

Status: Open.

#76 In LS-Lab/KeYmaeraX-release;

· rbohrer opened on May 19, 2021

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

UI

Status: Open.

#75 In LS-Lab/KeYmaeraX-release;

· rbohrer opened on May 13, 2021

Vector and Matrix Support

enhancement

Status: Open.

#69 In LS-Lab/KeYmaeraX-release;

· zstone1 opened on Sep 24, 2020