• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
        • Type-prescription
        • Rewrite
        • Meta
        • Linear
        • Definition
          • Force
            • Forcing-round
            • Failed-forcing
            • Immediate-force-modep
            • Disable-forcing
            • Enable-forcing
              • Disable-immediate-force-modep
              • Enable-immediate-force-modep
            • Syntaxp
            • Bind-free
            • Case-split
            • Simple
            • Set-body
            • Show-bodies
          • Clause-processor
          • Tau-system
          • Forward-chaining
          • Equivalence
          • Congruence
          • Free-variables
          • Executable-counterpart
          • Induction
          • Type-reasoning
          • Compound-recognizer
          • Rewrite-quoted-constant
          • Elim
          • Well-founded-relation-rule
          • Built-in-clause
          • Well-formedness-guarantee
          • Patterned-congruence
          • Rule-classes-introduction
          • Guard-holders
          • Refinement
          • Type-set-inverter
          • Generalize
          • Corollary
          • Induction-heuristics
          • Backchaining
          • Default-backchain-limit
        • Proof-builder
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Force

    Enable-forcing

    To allow forced case splits

    General Form:
ACL2 !>:enable-forcing    ; allowed forced case splits

    See force and see case-split for a discussion of forced case splits, which are turned back on by this command. See disable-forcing for an example showing how to turn off forced case splits.

    Enable-forcing is actually a macro that enables the executable-counterpart of the function symbol force; see force. When you want to use hints to turn on forced case splits, use a form such as one of the following (these are equivalent).

    :in-theory (enable (:executable-counterpart force))
:in-theory (enable (force))