Fgl-interp-obj
FGL testbench function to interpret a term that is the result of evaluating some form.
- Signature
(fgl-interp-obj term) → *
Logically, (fgl-interp-obj term) just returns NIL. When it is
encountered by the FGL interpreter under an unequiv congruence, it
recursively interprets the object that term evaluates to. That is, it
first interprets term, then if this results in a constant object whose
value is a pseudo-term, it interprets that and returns its result.
Definitions and Theorems
Function: fgl-interp-obj
(defun fgl-interp-obj (term)
(declare (xargs :guard t))
(let ((__function__ 'fgl-interp-obj))
(declare (ignorable __function__))
nil))
