• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
          • Emacs
        • About-ACL2
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • 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.