• 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