• 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
      • Startup
      • ACL2-as-standalone-program
      • Talks
      • Nqthm-to-ACL2
      • ACL2-sedan
        • Defunc
        • Cgen
        • Defdata
        • Ccg
        • Match
        • ACL2s-defaults
        • Definec
        • ACL2s-utilities
          • Make-n-ary-macro
          • N<
          • Test-then-skip-proofs
          • ACL2-pc::repeat-until-done
          • Thm-no-test
          • Defthm-no-test
      • Emacs
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• ACL2-sedan

ACL2s-utilities

Utilities used in ACL2s.

This is a collection of utilities used in ACL2s, the ACL2 Sedan.

Subtopics

Make-n-ary-macro

A macro that creates an arbitrary-arity macro given a binary function and associates the function name with the macro name using add-macro-fn.

N<

The well-founded less-than relation on natural numbers.

Test-then-skip-proofs

The ACL2s version of skip-proofs.

ACL2-pc::repeat-until-done

A proof-builder command that repeats the given instructions until all goals have been proved

Thm-no-test

A version of thm with testing disabled.

Defthm-no-test

A version of defthm with testing disabled.