|
|
|---|
|
|
|
|---|
A library about the ACL2 programming language.
The ACL2 theorem prover includes a programming language, which is essentially a subset of Common Lisp. ACL2 also includes a logical language, which is a superset of a subset of Common Lisp.
This library formalizes certain aspects of the syntax and semantics of the ACL2 programming language.
The formalization of the ACL2 evaluation semantics in this library is currently just the work of this library's author. It is not an official descripion of the ACL2 evaluation semantics in an analogous sense that this techical report is an official description of the ACL2 logical semantics. Refer to manual pages like this one for an official description of the ACL2 evaluation semantics.