• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
          • Tutorial1-towers-of-hanoi
          • Tutorial3-phonebook-example
          • Tutorial2-eights-problem
          • Solution-to-simple-example
          • Tutorial4-defun-sk-example
          • Tutorial5-miscellaneous-examples
            • Guard-example
            • Mutual-recursion-proof-example
            • Functional-instantiation-example
            • File-reading-example
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Tours
        • Emacs
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
        • Workshops
        • ACL2-tutorial
          • Introduction-to-the-theorem-prover
          • Pages Written Especially for the Tours
          • The-method
          • Advanced-features
          • Interesting-applications
          • Tips
          • Alternative-introduction
          • Tidbits
          • Annotated-ACL2-scripts
            • Tutorial1-towers-of-hanoi
            • Tutorial3-phonebook-example
            • Tutorial2-eights-problem
            • Solution-to-simple-example
            • Tutorial4-defun-sk-example
            • Tutorial5-miscellaneous-examples
              • Guard-example
              • Mutual-recursion-proof-example
              • Functional-instantiation-example
              • File-reading-example
          • Startup
          • ACL2-as-standalone-program
          • ACL2-sedan
          • Talks
          • Nqthm-to-ACL2
          • Tours
          • Emacs
        • Version
        • Acknowledgments
        • Using-ACL2
        • Releases
        • How-to-contribute
        • Pre-built-binary-distributions
        • Common-lisp
        • Installation
        • Mailing-lists
        • Git-quick-start
        • Copyright
        • ACL2-help
    • Miscellaneous
    • Output-controls
    • Bdd
    • Macros
    • Installation
    • Mailing-lists
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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

Guard-example

A brief transcript illustrating guards in ACL2

Mutual-recursion-proof-example

A small proof about mutually recursive functions

Functional-instantiation-example

A small proof demonstrating functional instantiation

File-reading-example

Example of reading files in ACL2