TUTORIAL5-MISCELLANEOUS-EXAMPLES

Major Section:  TUTORIAL-EXAMPLES

The following examples are more advanced examples of usage of ACL2. They are included largely for reference, in case someone finds them useful.

• FILE-READING-EXAMPLE -- example of reading files in ACL2

• FUNCTIONAL-INSTANTIATION-EXAMPLE -- a small proof demonstrating functional instantiation

• GUARD-EXAMPLE -- a brief transcript illustrating guards in ACL2

• MUTUAL-RECURSION-PROOF-EXAMPLE -- a small proof about mutually recursive functions