• 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

Set-default-hints

Set the default hints

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

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 set-default-hints! for a corresponding non-local event.

General Form:
(set-default-hints lst)

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

Whenever a defthm or thm command is executed, the default hints are appended to the right of any explicitly provided :hints in the command. The same applies to defuns as well (:hints, :guard-hints, and (for ACL2(r)) :std-hints). The hints are then translated and processed just as though they had been explicitly included.

Technically, we do not put restrictions on lst, beyond that it is a true list. It would be legal to execute

(set-default-hints '(("Goal" :use lemma23)))

with the effect that the given hint is added to subsequent hints supplied explicitly. An explicit "Goal" hint would, however, take priority, as suggested by the mention above of ``appended to the right.''

Note that set-default-hints sets the default hints as specified. To add to or remove from the current default, see add-default-hints and see remove-default-hints. To see the current default hints, 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!.

For a related feature, which however is only for advanced system builders, see override-hints.