A formalization of the ACL2 primitive functions.

The ACL2 primitive functions have no definitions. Their evaluation semantics is described in the ACL2 documentation.

In order to formalize the evaluation semantics of ACL2, we need to formalize the evaluation semantics of the primitive functions. We do so ``directly'' here, i.e. not via execution steps through evaluation states as we do for defined functions.

Since our formalization of the ACL2 primitive functions
is written in the ACL2 logical language,
we use the executable ACL2 primitive functions of the logical language
to formalize the ACL2 primitive functions of the ACL2 programming language.
However, note that the latter operate on our model of ACL2 values,
i.e. on the `value` fixtype,
while the former operate on ACL2 values directly.
So there is a necessary indirection there,
due to the meta level nature of our formalization.
The treatment of symbol values is also slightly different,
because, as noted in the documentation of `symbol-value`,
at the meta level we want to be able to talk about
all possible symbols for all possible known packages,
and not just the symbols for the packages that happen to be known
at the point in which we write this formalization.

Here we formalize the evaluation of the ACL2 primitive functions in the logic, i.e. for all possible values, inside and outside the guards. The treatment of values outside the guards are according to the completion axioms shown in the documentation, which amount to fixing the values to the required types.

- Eval-intern-in-package-of-symbol
- Evaluation semantics of
`intern-in-package-of-symbol`. - Eval-pkg-witness
- Evaluation semantics of
`pkg-witness`. - Eval-pkg-imports
- Evaluation semantics of
`pkg-imports`. - Primitive-function-namep
- Check if a symbol value is the name of a primitive function.
- Primitive-function-arity
- Arith of a primitive function.
- Eval-if
- Evaluation semantics of
`if`. - Eval-bad-atom<=
- Evaluation semantics of
bad-atom<= . - Eval-<
- Evaluation semantics of
`<`. - Eval-coerce
- Evaluation semantics of
`coerce`. - Eval-complex
- Evaluation semantics of
`complex`. - Eval-binary-+
- Evaluation semantics of
`binary-+`. - Eval-binary-*
- Evaluation semantics of
`binary-*`. - Eval-equal
- Evaluation semantics of
`equal`. - Eval-cons
- Evaluation semantics of
`cons`. - Eval-symbol-package-name
- Evaluation semantics of
`symbol-package-name`. - Eval-complex-rationalp
- Evaluation semantics of
`complex-rationalp`. - Eval-unary-/
- Evaluation semantics of
`unary-/`. - Eval-symbol-name
- Evaluation semantics of
`symbol-name`. - Eval-denominator
- Evaluation semantics of
`denominator`. - Eval-code-char
- Evaluation semantics of
`code-char`. - Eval-unary--
- Evaluation semantics of
`unary--`. - Eval-realpart
- Evaluation semantics of
`realpart`. - Eval-rationalp
- Evaluation semantics of
`rationalp`. - Eval-numerator
- Evaluation semantics of
`numerator`. - Eval-integerp
- Evaluation semantics of
`integerp`. - Eval-imagpart
- Evaluation semantics of
`imagpart`. - Eval-characterp
- Evaluation semantics of
`characterp`. - Eval-char-code
- Evaluation semantics of
`char-code`. - Eval-ACL2-numberp
- Evaluation semantics of
`ACL2-numberp`. - Eval-symbolp
- Evaluation semantics of
`symbolp`. - Eval-stringp
- Evaluation semantics of
`stringp`. - Eval-consp
- Evaluation semantics of
`consp`. - Eval-cdr
- Evaluation semantics of
`cdr`. - Eval-car
- Evaluation semantics of
`car`.