• 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
      • Defun
      • Verify-guards
      • Table
      • Mutual-recursion
      • Memoize
      • Make-event
      • Include-book
      • Encapsulate
      • Defun-sk
      • Defttag
      • Defstobj
      • Defpkg
      • Defattach
      • Defchoose
      • Defabsstobj
      • Progn
      • Verify-termination
      • Redundant-events
      • Defconst
      • 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
      • Deftheory-static
      • Defaxiom
      • Defund
      • Evisc-table
      • Verify-guards+
      • Logical-name
      • Profile
      • Defequiv
      • Defmacro-untouchable
      • Defthmr
      • Add-global-stobj
      • 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-custom-keyword-hint
      • Dft
      • Defthy
      • Remove-global-stobj
      • Defund-notinline
      • Defnd
      • Defn
      • Defund-inline
      • Defmacro-last
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defun
• Events

Defnd

disabled definition with guard t

Defnd is defund with guard t.

defnd expands to a defund with an added (declare (xargs :guard t)). If an explicit guard is supplied to defnd, it is conjoined to the added t guard, according to defun's treatment of multiple guard declarations.