• 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

• Hints

Default-hints

A list of hints added to every proof attempt

Examples:
ACL2 !>(default-hints (w state))
((computed-hint-1 clause)
 (computed-hint-2 clause stable-under-simplificationp))

The value returned by this function is added to the right of the :hints argument of every defthm and thm command, and to hints provided to defuns as well (:hints, :guard-hints, and (for ACL2(r)) :std-hints).

See set-default-hints for a more general discussion. Advanced users only: see override-hints for an advanced variant of default hints that are not superseded by :hints arguments.

Subtopics

Set-default-hints

Set the default hints

Add-default-hints

Add to the default hints

Remove-default-hints

Remove from the default hints

Default-hints-table

A table used to provide hints for proofs

Add-default-hints!

Add to the default hints non-locally

Set-default-hints!

Set the default hints non-locally

Remove-default-hints!

Remove from the default hints non-locally