		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mods->names

Signature
(elab-mods->names elab-mods) → names
Arguments: elab-mods — Guard (elab-modlist-p elab-mods).
Returns: names — Type (modnamelist-p names).

Definitions and Theorems

Function: elab-mods->names

(defun elab-mods->names (elab-mods)
  (declare (xargs :guard (elab-modlist-p elab-mods)))
  (let ((__function__ 'elab-mods->names))
    (declare (ignorable __function__))
    (if (atom elab-mods)
        nil
      (cons (modname-fix (g :name (car elab-mods)))
            (elab-mods->names (cdr elab-mods))))))

Theorem: modnamelist-p-of-elab-mods->names

(defthm modnamelist-p-of-elab-mods->names
  (b* ((names (elab-mods->names elab-mods)))
    (modnamelist-p names))
  :rule-classes :rewrite)

Theorem: elab-mods->names-of-elab-modlist-fix-elab-mods

(defthm elab-mods->names-of-elab-modlist-fix-elab-mods
  (equal (elab-mods->names (elab-modlist-fix elab-mods))
         (elab-mods->names elab-mods)))

Theorem: elab-mods->names-elab-modlist-equiv-congruence-on-elab-mods

(defthm elab-mods->names-elab-modlist-equiv-congruence-on-elab-mods
  (implies (elab-modlist-equiv elab-mods elab-mods-equiv)
           (equal (elab-mods->names elab-mods)
                  (elab-mods->names elab-mods-equiv)))
  :rule-classes :congruence)

Theorem: elab-mods->names-of-take

(defthm elab-mods->names-of-take
  (implies (<= (nfix n) (len elab-mods))
           (equal (elab-mods->names (take n elab-mods))
                  (take n (elab-mods->names elab-mods)))))

Theorem: len-of-elab-mods->names

(defthm len-of-elab-mods->names
  (equal (len (elab-mods->names x))
         (len x)))

Theorem: nth-of-elab-mods->names

(defthm nth-of-elab-mods->names
  (implies (< (nfix n) (len x))
           (equal (nth n (elab-mods->names x))
                  (modname-fix (g :name (nth n x))))))