• 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
    • Debugging
    • Miscellaneous
      • Term
      • Ld
      • Hints
        • Lemma-instance
        • Computed-hints
        • Override-hints
        • Hints-and-the-waterfall
        • Goal-spec
        • Termination-theorem-example
        • Consideration
        • Hint-wrapper
        • Default-hints
          • Set-default-hints
          • Add-default-hints
          • Remove-default-hints
          • Default-hints-table
          • Add-default-hints!
          • Set-default-hints!
          • Remove-default-hints!
        • Guard-theorem-example
        • Do-not-hint
        • Guard-theorem
        • Using-computed-hints
        • Termination-theorem
        • Custom-keyword-hints
        • Do-not
      • Type-set
      • Ordinals
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • 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
  • Math
  • Testing-utilities

• Default-hints

Remove-default-hints

Remove from the default hints

Examples:
(remove-default-hints '((computed-hint-1 clause)
                        (computed-hint-2 clause
                                         stable-under-simplificationp)))

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. It is local to the book or encapsulate form in which it occurs (see remove-default-hints! for a corresponding non-local event).

General Form:
(remove-default-hints lst)

where lst is a list. Generally speaking, the elements of lst should be suitable for use as computed-hints. Also see add-default-hints.

If some elements of the given list do not belong to the existing default hints, they will simply be ignored by this event.

Also See set-default-hints, see add-default-hints, and see default-hints.

Finally, note that the effects of set-default-hints, add-default-hints, and remove-default-hints are local to the book in which they appear. Thus, users who include a book with such forms will not have their default hints affected by such forms. In order to export the effect of setting the default hints, use set-default-hints!, add-default-hints!, or remove-default-hints!.