Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix typo in comment defining macros (#6306)
The existing comment describes macros as "formulas of the form `(forall X (= (f X) T[X]))` ... where `T[X]` does not contain `X`". This is incorrect; of course the macros' definitions are allowed to be in terms of the macros' arguments. The comment should say "...does not contain `f`" because macros can't be recursive.
- Loading branch information