An ACL2 library for C.

This library contains:

- A formalization of (a subset of) the C language. This is a deep embedding of C in ACL2.
- A representation of (a subset of) the C language constructs in ACL2. This is a shallow embedding of C in ACL2.
- A proof-generating C code generator for ACL2. This recognizes, and translates to C, the shallowly embedded ACL2 representation of C constructs, and generates proofs based on the deep embedding.

The library is work in progress.

This library is based on the ISO/IEC 9899:2018 specification of C. In the documentation of this library, this standard is referenced as `[C]'; sections are referenced by appending their designations separated by colon, e.g. `[C:6.2.6]' references Section 6.2.6; paragraphs are referenced by further appending their numbers separated by slash, e.g. `[C:6.2.5/2]' references Paragraph 2 of Section 6.2.5. These square-bracketed references may be used as nouns or parenthetically.

- Atc
- ATC (
**A**CL2**T**o**C**), a proof-generating C code generator for ACL2. - Language
- A formal model of (a subset of) the C language.
- Representation
- A representation of C in ACL2.
- Pack
- Build a symbol in the C package from a list of atoms.