Turn a field into a typed variable.
(field-to-typed-variable field) → var
Sometimes fields are used as variables, in particular in invariants of product and sum types. Fields and typed variables are isomorphic. This function converts the former to the latter.
Function:
(defun field-to-typed-variable (field) (declare (xargs :guard (fieldp field))) (let ((__function__ 'field-to-typed-variable)) (declare (ignorable __function__)) (make-typed-variable :name (field->name field) :type (field->type field))))
Theorem:
(defthm typed-variablep-of-field-to-typed-variable (b* ((var (field-to-typed-variable field))) (typed-variablep var)) :rule-classes :rewrite)
Theorem:
(defthm field-to-typed-variable-of-field-fix-field (equal (field-to-typed-variable (field-fix field)) (field-to-typed-variable field)))
Theorem:
(defthm field-to-typed-variable-field-equiv-congruence-on-field (implies (field-equiv field field-equiv) (equal (field-to-typed-variable field) (field-to-typed-variable field-equiv))) :rule-classes :congruence)