|
|
|---|
|
|
|
|---|
Define a GL clause processor with a given set of built-in symbolic counterparts.
Usage:
(def-gl-clause-processor my-gl-clause-processor :output with-output-settings)
The above form defines a GL clause processor function named my-gl-clause-processor. This clause processor is defined so that it can execute all existing symbolic counterpart functions.
If one adds symbolic counterpart functions, either by hand-coding them, using make-g-world, or including books that add them, one will need to define a new GL clause processor.
Each GL clause processor has an associated sets of functions that it can directly execute symbolically. DEF-GL-CLAUSE-PROCESSOR makes a new processor that can execute the full set of existing symbolic counterparts. (Symbolic counterparts may be defined by hand or using make-g-world.)
It used to be the case that the clause processor also had a fixed set of functions it could execute concretely. That is no longer the case. We still accept the old form of def-gl-clause-processor, which takes an additional argument after the name of the clause processor and before the :output keyword (if any). However, this is deprecated and a message will be printed saying so.
See def-gl-thm and gl-hint for information on using the GL clause processor to prove theorems.