• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
      • Install-not-normalized-event
      • Install-not-normalized-event-lst
      • Install-not-normalized$
    • Rewrite$
    • Removable-runes
    • Efficiency
    • Bash
    • Def-dag-measure
    • Fgl
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/system
• Install-not-normalized

Install-not-normalized$

Install the non-normalized definition of a function, ensuring that the name of the theorem will not cause a conflict.

This utility is an event which, when evaluated successfully, installs the event generated by install-not-normalized-event. See install-not-normalized-event.

This is related to install-not-normalized.

Macro: install-not-normalized$

(defmacro
 install-not-normalized$
 (fn &key allp names-to-avoid)
 (cons
      'make-event
      (cons (cons 'install-not-normalized$-fn
                  (cons (cons 'quote (cons fn 'nil))
                        (cons allp (cons names-to-avoid '(state)))))
            'nil)))