Narrow-equiv
FGL testbench function to interpret a term under a narrower (stricter) equivalence context.
- Signature
(narrow-equiv equiv val) → *
Logically, (narrow-equiv equiv val) just returns val.
When it is encountered by the FGL interpreter and equiv evaluates to an
equiv-contexts-p object that is a more granular equivalence than the
current equivalence context, then it interprets val under an equiv
congruence. The most relevant equiv-contexts objects:
- nil means rewrite under equal, that is, an object is only equivalent to itself
- (iff) means rewrite under iff
- (unequiv) means rewrite under unequiv, that is, all objects are equivalent.
Definitions and Theorems
Function: narrow-equiv
(defun narrow-equiv (equiv val)
(declare (xargs :guard t))
(let ((__function__ 'narrow-equiv))
(declare (ignorable __function__))
val))
