|
|
|---|
|
|
|
|---|
Fixtype of bindings.
We formalize a binding of variables to values as an omap from symbols to values. In our formalization of translated terms, variables are identified by symbol values; so we use symbol values as the keys of the omaps that formalize bindings.
Theorem:
(defthm bindingp-of-from-lists (implies (and (symbol-value-listp variables) (value-listp values) (equal (len variables) (len values))) (bindingp (omap::from-lists variables values))))