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