• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
        • Type-prescription
        • Rewrite
        • Meta
        • Linear
        • Definition
        • Clause-processor
        • Tau-system
        • Forward-chaining
        • Equivalence
        • Congruence
        • Free-variables
        • Executable-counterpart
        • Induction
          • Induction-depth-limit
          • Set-induction-depth-limit!
          • 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
    • Induction

    Set-induction-depth-limit!

    Set the induction-depth-limit non-locally

    Please see set-induction-depth-limit, which is the same as set-induction-depth-limit! except that the latter is not local to the encapsulate or the book in which it occurs. Probably set-induction-depth-limit is to be preferred unless you have a good reason for wanting to export the effect of this event outside the enclosing encapsulate or book.