Skip to content

Add optional term argument to hints #159

@andrew-johnson-4

Description

@andrew-johnson-4

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

No one assigned

    Labels

    checkerIssues related to Typechecking or LogicenhancementNew feature or requestparserIssues related to Tokenization or Parsing

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions