Generate shallowly embedded formal parameters for the function synonyms generated by atj-gen-shallow-synonym-method.
(atj-gen-shallow-synonym-method-params n) → formals
The exact formal parameters are not important,
so for now we just generate
Function:
(defun atj-gen-shallow-synonym-method-params-aux (n acc) (declare (xargs :guard (and (natp n) (string-listp acc)))) (let ((__function__ 'atj-gen-shallow-synonym-method-params-aux)) (declare (ignorable __function__)) (cond ((zp n) acc) (t (atj-gen-shallow-synonym-method-params-aux (1- n) (cons (str::cat "x" (nat-to-dec-string n)) acc))))))
Theorem:
(defthm string-listp-of-atj-gen-shallow-synonym-method-params-aux (implies (string-listp acc) (b* ((formals (atj-gen-shallow-synonym-method-params-aux n acc))) (string-listp formals))) :rule-classes :rewrite)
Function:
(defun atj-gen-shallow-synonym-method-params (n) (declare (xargs :guard (natp n))) (let ((__function__ 'atj-gen-shallow-synonym-method-params)) (declare (ignorable __function__)) (atj-gen-shallow-synonym-method-params-aux n nil)))
Theorem:
(defthm string-listp-of-atj-gen-shallow-synonym-method-params (b* ((formals (atj-gen-shallow-synonym-method-params n))) (string-listp formals)) :rule-classes :rewrite)