		Search-engine friendly clone of the ACL2 documentation.

Number-theory

Defprime-alias

Introduce an alias of an existing prime introduced with defprime.

General Form:

(defprime-alias name
                existing-prime-name
                &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.

existing-prime-name — (required)

Name of the existing prime, a symbol.

: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-alias generates all of the things generated by defprime, except that it omits the call to ACL2::add-io-pairs, since that has already been done for the existing prime, which has the same numeric value as the new prime.