Indexed-subst-templates
- Signature
(indexed-subst-templates name from by how-many &key
(base-subst '(acl2::make-tmplsubst)))
→
*- Arguments
- name — Guard (symbolp name).
- from — Guard (integerp from).
- by — Guard (integerp by).
- how-many — Guard (natp how-many).
- base-subst — Guard (acl2::tmplsubst-p base-subst).
Definitions and Theorems
Function: indexed-subst-templates-fn
(defun indexed-subst-templates-fn (name from by how-many base-subst)
(declare (xargs :guard (and (symbolp name)
(integerp from)
(integerp by)
(natp how-many)
(acl2::tmplsubst-p base-subst))))
(let ((__function__ 'indexed-subst-templates))
(declare (ignorable __function__))
(if (zp how-many)
nil
(cons
(b* (((acl2::tmplsubst base-subst)))
(acl2::change-tmplsubst
base-subst
:atoms (append (cons (cons name from) 'nil)
base-subst.atoms)
:strs
(append (cons (cons (symbol-name name)
(coerce (explode-atom from 10) 'string))
'nil)
base-subst.strs)))
(indexed-subst-templates name (+ from by)
by (1- how-many)
:base-subst base-subst)))))
