• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
      • Real
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
        • Advanced-features
        • The-method
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
          • Tutorial3-phonebook-example
          • Tutorial1-towers-of-hanoi
          • Tutorial2-eights-problem
          • Solution-to-simple-example
          • Tutorial4-defun-sk-example
          • Tutorial5-miscellaneous-examples
            • Mutual-recursion-proof-example
            • Guard-example
            • Functional-instantiation-example
            • File-reading-example
        • Startup
        • ACL2-as-standalone-program
        • Talks
        • Nqthm-to-ACL2
        • ACL2-sedan
        • Emacs
      • Debugging
      • Miscellaneous
      • Output-controls
      • Built-in-theorems
      • Macros
      • Interfacing-tools
      • About-ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Annotated-ACL2-scripts

Tutorial5-miscellaneous-examples

Miscellaneous ACL2 examples

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

Subtopics

Mutual-recursion-proof-example
A small proof about mutually recursive functions
Guard-example
A brief transcript illustrating guards in ACL2
Functional-instantiation-example
A small proof demonstrating functional instantiation
File-reading-example
Example of reading files in ACL2