• 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
          • Xargs
          • 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
          • Verify-termination
          • Redundant-events
          • Defmacro
          • Defconst
          • 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
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Defun
      • Events

      Defund-nx

      Define a disabled non-executable function symbol

      Use defund-nx instead of defun-nx when you want to disable the definition of a function symbol immediately after defining it in :logic mode. In all other respects, defund-nx has the same behavior as defun-nx; See defun-nx for details. Also see defund.