• 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
    • ACL2s-utilities
    • Cgen

    Test-then-skip-proofs

    The ACL2s version of skip-proofs.

    A macro that is similar to skip-proofs, except that we first perform testing. The macro supports testing for thm, defthm, defcong, defequiv, and defrefinement forms. All other forms are just turned into skip-proofs forms, without testing.