-
-
Notifications
You must be signed in to change notification settings - Fork 3
Open
Labels
checkerIssues related to Typechecking or LogicIssues related to Typechecking or LogicenhancementNew feature or requestNew feature or requestparserIssues related to Tokenization or ParsingIssues related to Tokenization or Parsing
Milestone
Description
Is your feature request related to a problem? Please describe.
Hints may need to be parameterized to prove a goal. This parameter should be a single term so that hints can nest inside of other hints.
Describe the solution you'd like
//axioms
axiom @reflexive a. [True] = a == a;
axiom @symmetric a, b. [True] = a == b => b == a;
axiom @transitive a, b, c. [True] = a == b && b == c => a == c;
x == z @transitive(x == y && y == z)
Metadata
Metadata
Assignees
Labels
checkerIssues related to Typechecking or LogicIssues related to Typechecking or LogicenhancementNew feature or requestNew feature or requestparserIssues related to Tokenization or ParsingIssues related to Tokenization or Parsing