• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
      • Start-here
      • Real
      • Debugging
      • Miscellaneous
        • Term
        • Ld
        • Hints
          • Lemma-instance
          • Computed-hints
          • Override-hints
            • Add-override-hints
              • Remove-override-hints
              • Set-override-hints
              • Remove-override-hints!
              • Set-override-hints!
              • Add-override-hints!
            • Hints-and-the-waterfall
            • Goal-spec
            • Termination-theorem-example
            • Consideration
            • Hint-wrapper
            • Default-hints
            • Guard-theorem-example
            • Do-not-hint
            • Guard-theorem
            • Using-computed-hints
            • Termination-theorem
            • Custom-keyword-hints
            • Do-not
          • Type-set
          • Ordinals
          • ACL2-customization
          • With-prover-step-limit
          • With-prover-time-limit
          • Set-prover-step-limit
          • Local-incompatibility
          • Set-case-split-limitations
          • Subversive-recursions
          • Specious-simplification
          • Defsum
          • Oracle-timelimit
          • Thm
          • Defopener
          • Gcl
          • Case-split-limitations
          • Set-gc-strategy
          • Default-defun-mode
          • Top-level
          • Reader
          • Ttags-seen
          • Adviser
          • Ttree
          • Abort-soft
          • Defsums
          • Gc$
          • With-timeout
          • Coi-debug::fail
          • Expander
          • Gc-strategy
          • Coi-debug::assert
          • Sin-cos
          • Def::doc
          • Syntax
          • Subversive-inductions
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Override-hints

    Add-override-hints

    Add to the override-hints

    See override-hints for a discussion of override-hints. Here we describe how to extend the list of override-hints. Note that the effects of add-override-hints events are local to the books or encapsulate events in which they reside; see add-override-hints! to avoid that restriction. Also see set-override-hints to set a new list of override-hints to it, ignoring the present list rather than adding to it.

    General Forms:
    (add-override-hints form)
    (add-override-hints form :at-end t)
    (add-override-hints form :at-end nil) ; default for :at-end

    where form evaluates to a list of computed hint forms. The effect of this event is to extend the current list of override-hints by appending the result of that evaluation. The default is to append the evaluation result to the front of the current list of override-hints, but if :at-end t is specified, then the evaluation result is appended to the end of the current list.