		Search-engine friendly clone of the ACL2 documentation.

Esim-vl

Esim-vl-annotations

Helper for esim-vl-designwires and esim-vl-wirealist.

Definitions and Theorems

Function: esim-vl-annotations

(defun esim-vl-annotations (mod)
 (declare (xargs :guard t))
 (b*
  ((name (gpl :n mod))
   ((unless name)
    (er
     hard? 'esim-vl-annotations
     "Expected an E module, but this object doesn't even have a :n ~
               field: ~x0.~%"
     mod))
   (annotations (gpl :a mod))
   ((unless (alistp annotations))
    (er hard? 'esim-vl-annotations
        "In E module ~s0, the annotations field :a is not an alist."
        name)))
  annotations))

Theorem: alistp-of-esim-vl-annotations

(defthm alistp-of-esim-vl-annotations
  (alistp (esim-vl-annotations mod)))