Bind-var
Form that can bind a free variable to the result of an arbitrary computation.
- Signature
(bind-var ans form) → *
Logically, (bind-var var form) just returns var.
However, in FGL, the intended use is to bind a free variable in a rewrite rule
to the result of some arbitrary computation. The form argument is
rewritten under an unequiv congruence so it can do extralogical things
like examining the interpreter state and term syntax. The var argument
must be a variable that hasn't yet been bound during the application of the
current rewrite rule.
Definitions and Theorems
Function: bind-var
(defun bind-var (ans form)
(declare (xargs :guard t))
(let ((__function__ 'bind-var))
(declare (ignorable __function__))
ans))
Theorem: unequiv-implies-equal-bind-var-2
(defthm unequiv-implies-equal-bind-var-2
(implies (unequiv form form-equiv)
(equal (bind-var ans form)
(bind-var ans form-equiv)))
:rule-classes (:congruence))
Theorem: bind-var-binder-rule
(defthm bind-var-binder-rule
(implies (equal ans form)
(equal (bind-var ans form) ans)))
