		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

Map-address-ident-list

Map c$::expr-unary c$::unop-address over a list of identifiers.

Signature
(map-address-ident-list idents) → exprs
Arguments: idents — Guard (ident-listp idents).
Returns: exprs — Type (expr-listp exprs).

Definitions and Theorems

Function: map-address-ident-list

(defun map-address-ident-list (idents)
 (declare (xargs :guard (ident-listp idents)))
 (if (endp idents)
     nil
  (cons
      (make-expr-unary :op (c$::unop-address)
                       :arg (make-expr-ident :ident (first idents)))
      (map-address-ident-list (rest idents)))))

Theorem: expr-listp-of-map-address-ident-list

(defthm expr-listp-of-map-address-ident-list
  (b* ((exprs (map-address-ident-list idents)))
    (expr-listp exprs))
  :rule-classes :rewrite)