		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Initializers-to-variable-substitution

Turn a list of initializers into a variable substitution.

Signature
(initializers-to-variable-substitution inits) → subst
Arguments: inits — Guard (initializer-listp inits).
Returns: subst — Type (variable-substitutionp subst).

Each field name is regarded as a variable and the corresponding expression is associated to the variable, and will replace the variable when the substitution is applied.

Definitions and Theorems

Function: initializers-to-variable-substitution

(defun initializers-to-variable-substitution (inits)
 (declare (xargs :guard (initializer-listp inits)))
 (let ((__function__ 'initializers-to-variable-substitution))
  (declare (ignorable __function__))
  (cond
    ((endp inits) nil)
    (t (omap::update
            (initializer->field (car inits))
            (initializer->value (car inits))
            (initializers-to-variable-substitution (cdr inits)))))))

Theorem: variable-substitutionp-of-initializers-to-variable-substitution

(defthm
    variable-substitutionp-of-initializers-to-variable-substitution
  (b* ((subst (initializers-to-variable-substitution inits)))
    (variable-substitutionp subst))
  :rule-classes :rewrite)

Theorem: initializers-to-variable-substitution-of-initializer-list-fix-inits

(defthm
 initializers-to-variable-substitution-of-initializer-list-fix-inits
 (equal (initializers-to-variable-substitution
             (initializer-list-fix inits))
        (initializers-to-variable-substitution inits)))

Theorem: initializers-to-variable-substitution-initializer-list-equiv-congruence-on-inits

(defthm
 initializers-to-variable-substitution-initializer-list-equiv-congruence-on-inits
 (implies
      (initializer-list-equiv inits inits-equiv)
      (equal (initializers-to-variable-substitution inits)
             (initializers-to-variable-substitution inits-equiv)))
 :rule-classes :congruence)