Introduce an alias of an existing prime introduced with defprime.
(defprime-alias name existing-prime-name &key :evisc ; default t :parents ; default :auto :short ; default :auto :long ; default :auto :doc ; default t )
Name of the prime to introduce, a symbol.
Name of the existing prime, a symbol.
Whether to print occurrences of the prime using its symbolic name.
Xdoc :parents for the prime.
Xdoc :short description for the prime.
Xdoc :long section for the prime.
Whether to generate xdoc for the prime.
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.