• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
      • Defun
        • Xargs
          • Guard
            • Verify-guards
            • Mbe
            • Set-guard-checking
            • Ec-call
            • Print-gv
            • The
            • Guards-and-evaluation
            • Guard-debug
            • Set-check-invariant-risk
            • Guard-evaluation-table
            • Guard-evaluation-examples-log
            • Guard-example
            • Defthmg
            • Invariant-risk
            • With-guard-checking
            • Guard-miscellany
            • Guard-holders
            • Guard-formula-utilities
            • Set-verify-guards-eagerness
            • Guard-quick-reference
            • Set-register-invariant-risk
            • Guards-for-specification
            • Guard-evaluation-examples-script
            • Guard-introduction
            • Program-only
            • Non-exec
            • Set-guard-msg
            • Safe-mode
            • Set-print-gv-defaults
            • Guard-theorem-example
            • With-guard-checking-event
            • With-guard-checking-error-triple
            • Guard-checking-inhibited
            • Extra-info
          • Otf-flg
          • Normalize
          • Measure
        • Mutual-recursion
        • Defun-mode
        • Rulers
        • Defun-inline
        • Defun-nx
        • Defund
        • Set-ignore-ok
        • Set-well-founded-relation
        • Set-measure-function
        • Set-irrelevant-formals-ok
        • Defun-notinline
        • Set-bogus-defun-hints-ok
        • Defund-nx
        • Defun$
        • Defund-notinline
        • Defnd
        • Defn
        • Defund-inline
        • Set-bogus-measure-ok
      • Verify-guards
      • Table
      • Mutual-recursion
      • Memoize
      • Make-event
      • Include-book
      • Encapsulate
      • Defun-sk
      • Defttag
      • Defstobj
      • Defpkg
      • Defattach
      • Defabsstobj
      • Defchoose
      • Progn
      • Defconst
      • Verify-termination
      • Redundant-events
      • Defmacro
      • Skip-proofs
      • In-theory
      • Embedded-event-form
      • Value-triple
      • Comp
      • Local
      • Defthm
      • Progn!
      • Defevaluator
      • Theory-invariant
      • Assert-event
      • Defun-inline
      • Project-dir-alist
      • Partial-encapsulate
      • Define-trusted-clause-processor
      • Defproxy
      • Defexec
      • Defun-nx
      • Defthmg
      • Defpun
      • Defabbrev
      • Set-table-guard
      • Name
      • Defrec
      • Add-custom-keyword-hint
      • Regenerate-tau-database
      • Defcong
      • Deftheory
      • Defaxiom
      • Deftheory-static
      • Defund
      • Evisc-table
      • Verify-guards+
      • Logical-name
      • Profile
      • Defequiv
      • Defmacro-untouchable
      • Add-global-stobj
      • Defthmr
      • Defstub
      • Defrefinement
      • Deflabel
      • In-arithmetic-theory
      • Unmemoize
      • Defabsstobj-missing-events
      • Defthmd
      • Fake-event
      • Set-body
      • Defun-notinline
      • Functions-after
      • Macros-after
      • Dump-events
      • Defund-nx
      • Defun$
      • Remove-global-stobj
      • Remove-custom-keyword-hint
      • Dft
      • Defthy
      • Defund-notinline
      • Defnd
      • Defn
      • Defund-inline
      • Defmacro-last
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Miscellaneous
    • Output-controls
    • Bdd
    • Macros
    • Installation
    • Mailing-lists
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Guard

Extra-info

Sources of measure, guard, or constraint proof obligations

(Extra-info x y) always returns t by definition. See guard-debug and see measure-debug for a discussion of this function, which is useful for debugging failures from attempts to prove measure conjectures or to verify guards. See set-constraint-tracking to see how extra-info can help in debugging failures to prove constraint obligations generated by :functional-instance hints (see lemma-instance).