		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Create-elab-mod$a

Signature
(create-elab-mod$a) → elab-mod$a
Returns: elab-mod$a — Type (elab-mod$ap elab-mod$a).

Definitions and Theorems

Function: create-elab-mod$a

(defun create-elab-mod$a nil
  (declare (xargs :guard t))
  (let ((__function__ 'create-elab-mod$a))
    (declare (ignorable __function__))
    (b* ((m (s :name "default-modname" nil))
         (m (s :totalwires 0 m))
         (m (s :totalinsts 0 m))
         (m (s :orig-mod (make-module) m)))
      m)))

Theorem: elab-mod$ap-of-create-elab-mod$a

(defthm elab-mod$ap-of-create-elab-mod$a
  (b* ((elab-mod$a (create-elab-mod$a)))
    (elab-mod$ap elab-mod$a))
  :rule-classes :rewrite)