		Search-engine friendly clone of the ACL2 documentation.

Sexpr-rewriting-internals

Sexpr-unify: Unifies an S-expression with a pattern and returns the resulting substitution as an alist binding variables to subterms.
Sexpr-rewrite: Applies inside-out rewriting to an s-expression using a user-provided set of rewrite rules.
Sexpr-rewrite-try-rules: Given the args of a term and a list of possible rewrites for terms with the same top function symbol, tries each of the rewrites until one matches.
Sexpr-rewrite-ground: Checks whether the given s-expression's arguments are all constants, and if so, rewrites it to a constant by evaluating it under the empty environment.
4v-sexpr-compose-nofal: Identical to 4v-sexpr-compose, but not memoized and does not use fast alist lookups.
Sexpr-rewrite-sigma: Apply sexpr-rewriting to an sexpr with a substitution. The expressions in the substitution are assumed to already be simplified.
Sexpr-rewrite-fncall: Apply sexpr-rewriting to a function applied to some args, which are assumed to already be simplified.