Rules for init-scope.
The base case is a call
We need to enable eq because it arises from
the translation of
Theorem:
(defthm init-scope-when-consp (implies (and (syntaxp (quotep formals)) (consp formals) (equal formal (car formals)) (param-declonp formal) (valuep val) (not (equal (value-kind val) :array)) (equal name+tyname (param-declon-to-ident+tyname formal)) (equal name (mv-nth 0 name+tyname)) (equal tyname (mv-nth 1 name+tyname)) (equal (type-of-value val) (adjust-type (tyname-to-type tyname))) (value-listp vals) (equal scope (init-scope (cdr formals) vals)) (scopep scope) (not (omap::assoc name scope))) (equal (init-scope formals (cons val vals)) (omap::update name (remove-flexible-array-member val) scope))))