|
|
|---|
|
|
|
|---|
Add a new pattern to the untranslate patterns table.
General Form:
(add-untranslate-pattern target replacement)
Examples:
(add-untranslate-pattern-function '(1 2 3) *myconst*) (add-untranslate-pattern-function (f$ ?a ?b mystobj) (f a b))
We add a new pattern to the untranslate patterns table. The target should be either a quoted constant (which must be fully expanded, it does not get evaluated), or an unquoted function call.
The first example above changes proof output so that the constant '(1 2 3)
is instead printed as *myconst*. The second example changes proof output so
that for all