Assume
FGL testbench function to assume some condition while interpreting a term.
- Signature
(assume test val) → *
Logically, (assume test val) just returns NIL. When it is
encountered by the FGL interpreter under an unequiv congruence, it
causes the interpreter to assume that test is true while interpreting
val, returning the symbolic result from val.
Definitions and Theorems
Function: assume
(defun assume (test val)
(declare (xargs :guard t))
(let ((__function__ 'assume))
(declare (ignorable __function__))
nil))
