Defprime
Introduce a prime and related machinery.
General Form:
(defprime name
number
pratt-cert
&key
:evisc ; default t
:parents ; default :auto
:short ; default :auto
:long ; default :auto
:doc ; default t
)
Inputs:
name — (required)
Name of the prime to introduce, a symbol.
number — (required)
Numeric value of the prime, a natural number.
pratt-cert — (required)
Pratt certificate for the prime.
:evisc — default t
Whether to print occurrences of the prime using its symbolic name.
:parents — default :auto
Xdoc :parents for the prime.
:short — default :auto
Xdoc :short description for the prime.
:long — default :auto
Xdoc :long section for the prime.
:doc — default t
Whether to generate xdoc for the prime.
Description:
Defprime generates, for a prime named FOO:
- A constant, *FOO*, representing the prime.
- A theorem that *FOO* is prime.
- A 0-ary function, FOO, representing the prime. This is disabled but its :executable-counterpart is not (disable the :executable-counterpart to prevent execution during proofs).
- A theorem that the function FOO always returns a prime.
- A :linear rule stating that the function FOO is equal to the prime (i.e., its integer value).
- A utility, eviscerate-FOO, to cause the prime to be printed using a symbolic name. This is in turn invoked by defprime to turn on evisceration, unless the :evisc argument is nil.
- A utility, uneviscerate-FOO, to turn off the evisceration mentioned just above.
- A constant, *FOO-pratt-cert*, for the Pratt certificate supplied for FOO.
- A defxdoc form for the prime, using the supplied :short, :long, and :parents, or suitable defaults for each.
- A call of ACL2::add-io-pairs to cause primep to be fast when called on the prime.
- A table event that records the call of defprime.
