		Search-engine friendly clone of the ACL2 documentation.

Split-fn

Make-deref-subst

Signature
(make-deref-subst idents) → subst
Arguments: idents — Guard (ident-listp idents).
Returns: subst — Type (ident-expr-mapp subst).

Definitions and Theorems

Function: make-deref-subst

(defun make-deref-subst (idents)
 (declare (xargs :guard (ident-listp idents)))
 (if (endp idents)
     nil
  (omap::update
   (ident-fix (first idents))
   (expr-paren
     (make-expr-unary :op (c$::unop-indir)
                      :arg (make-expr-ident :ident (first idents))))
   (make-deref-subst (rest idents)))))

Theorem: ident-expr-mapp-of-make-deref-subst

(defthm ident-expr-mapp-of-make-deref-subst
  (b* ((subst (make-deref-subst idents)))
    (ident-expr-mapp subst))
  :rule-classes :rewrite)