Uguard
Unoptimized guard of a named function or of a lambda expression.
- Signature
(uguard fn wrld) → guard
- Arguments
- fn — Guard (pseudo-termfnp fn).
- wrld — Guard (plist-worldp wrld).
- Returns
- guard — A pseudo-termp.
This is a specialization of guard with nil as the second argument.
Since guard is in program mode only because of
the code that handles the case in which
the second argument is non-nil,
we avoid calling guard and instead replicate
the code that handles the case in which the second argument is nil;
thus, this utility is in logic mode and guard-verified.
See uguard+ for an enhanced variant of this utility.
Definitions and Theorems
Function: uguard
(defun uguard (fn wrld)
(declare (xargs :guard (and (pseudo-termfnp fn)
(plist-worldp wrld))))
(let ((__function__ 'uguard))
(declare (ignorable __function__))
(cond ((symbolp fn)
(getpropc fn 'guard *t* wrld))
(t *t*))))
