• 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
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
          • Defunc
          • Cgen
          • Ccg
          • Defdata
          • ACL2s-user-guide
          • ACL2s-tutorial
          • ACL2s-implementation-notes
          • Match
          • ACL2s-faq
          • ACL2s-intro
          • ACL2s-defaults
          • Definec
          • ACL2s-utilities
            • Make-n-ary-macro
            • Remove-dups
            • ACL2-pc::instantiate
            • N<
            • Test-then-skip-proofs
            • ACL2-pc::claim-simple
            • ACL2-pc::pro-or-skip
            • ACL2-pc::retain-or-skip
            • ACL2-pc::repeat-until-done
            • ACL2-pc::drop-or-skip
            • ACL2-pc::cg-or-skip
            • ACL2-pc::by
            • ACL2-pc::split-in-theory
            • Thm-no-test
            • Defthmd-no-test
            • Defthm-no-test
          • ACL2s-interface
          • ACL2s-installation
        • 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
          • Startup
          • ACL2-as-standalone-program
          • ACL2-sedan
            • Defunc
            • Cgen
            • Ccg
            • Defdata
            • ACL2s-user-guide
            • ACL2s-tutorial
            • ACL2s-implementation-notes
            • Match
            • ACL2s-faq
            • ACL2s-intro
            • ACL2s-defaults
            • Definec
            • ACL2s-utilities
              • Make-n-ary-macro
              • Remove-dups
              • ACL2-pc::instantiate
              • N<
              • Test-then-skip-proofs
              • ACL2-pc::claim-simple
              • ACL2-pc::pro-or-skip
              • ACL2-pc::retain-or-skip
              • ACL2-pc::repeat-until-done
              • ACL2-pc::drop-or-skip
              • ACL2-pc::cg-or-skip
              • ACL2-pc::by
              • ACL2-pc::split-in-theory
              • Thm-no-test
              • Defthmd-no-test
              • Defthm-no-test
            • ACL2s-interface
            • ACL2s-installation
          • 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

• 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.

Remove-dups

Remove duplicates from a true list and maintain the order of elements.

ACL2-pc::instantiate

Instantiate a theorem

N<

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

Test-then-skip-proofs

The ACL2s version of skip-proofs.

ACL2-pc::claim-simple

(atomic macro) add a new hypothesis, without promotion

ACL2-pc::pro-or-skip

(atomic macro) repeatedly apply promote, if possible

ACL2-pc::retain-or-skip

(atomic macro) drop all but the indicated top-level hypotheses

ACL2-pc::repeat-until-done

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

ACL2-pc::drop-or-skip

(atomic macro) drop top-level hypotheses

ACL2-pc::cg-or-skip

(atomic macro) change goals when needed

ACL2-pc::by

(atomic macro) prove using an existing theorem

ACL2-pc::split-in-theory

Split using an optional theory

Thm-no-test

A version of thm with testing disabled.

Defthmd-no-test

A version of defthmd with testing disabled.

Defthm-no-test

A version of defthm with testing disabled.