Search results

Support for Coq's tactic syntax (., ;)

Status: Open.

#84 In kframework/matching-logic-prover;

· h0nzZik opened on Aug 11, 2020

Delete the rest of the prover (in the notation branch).

Status: Open.

#83 In kframework/matching-logic-prover;

· h0nzZik opened on Aug 11, 2020

Syntactic matching for the apply strategy.

Status: Open.

#82 In kframework/matching-logic-prover;

· h0nzZik opened on Aug 11, 2020

Merge symbolic unit tests and unit-test semantics

Status: Open.

#75 In kframework/matching-logic-prover;

· nishantjr opened on Jun 13, 2020

Deterministic choice operators

Status: Open.

#63 In kframework/matching-logic-prover;

· nishantjr opened on Apr 22, 2020

Axiom names are duplicated

Status: Open.

#52 In kframework/matching-logic-prover;

· nishantjr opened on Mar 23, 2020

Replace \hole() with #hole

Status: Open.

#49 In kframework/matching-logic-prover;

· h0nzZik opened on Mar 10, 2020

Matchig variables - duplicated rule

Status: Open.

#48 In kframework/matching-logic-prover;

· h0nzZik opened on Feb 25, 2020

apply-equation should check functionality of terms in substitution

Status: Open.

#47 In kframework/matching-logic-prover;

· h0nzZik opened on Feb 25, 2020

replace-svar-with-constant

Status: Open.

#46 In kframework/matching-logic-prover;

· h0nzZik opened on Feb 18, 2020

Remove the ability to have unnamed axioms.

Status: Open.

#45 In kframework/matching-logic-prover;

· h0nzZik opened on Feb 11, 2020

match strategy working with axioms and arbitrary formulas

Status: Open.

#44 In kframework/matching-logic-prover;

· h0nzZik opened on Feb 11, 2020