Skip to content

Commit

Permalink
README: clarify syntax of local composite terms
Browse files Browse the repository at this point in the history
  • Loading branch information
JLimperg committed Feb 21, 2024
1 parent a185276 commit 62001c2
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -398,8 +398,10 @@ proved its goal already or which can never prove its goal. More formally:
A **rule builder** is a metaprogram that turns an expression into an Aesop rule.
When you tag a declaration with the `@[aesop]` attribute, the builder is applied
to the declared constant. When you use the `add` clause, as in `(add <phase>
<builder> <term>)`, the builder is applied to the given term, which may involve
hypotheses from the goal. However, some builders only support global constants.
<builder> (<term>))`, the builder is applied to the given term, which may
involve hypotheses from the goal. However, some builders only support global
constants. If the `term` is a single identifier, e.g. the name of a hypothesis,
the parentheses around it are optional.

Currently available builders are:

Expand Down

0 comments on commit 62001c2

Please sign in to comment.