Elab-mod$ap
- Signature
(elab-mod$ap elab-mod$a) → *
Definitions and Theorems
Function: elab-mod$ap
(defun elab-mod$ap (elab-mod$a)
(declare (xargs :guard t))
(let ((__function__ 'elab-mod$ap))
(declare (ignorable __function__))
(b* ((name (g :name elab-mod$a))
(totalwires (g :totalwires elab-mod$a))
(totalinsts (g :totalinsts elab-mod$a))
(orig-mod (g :orig-mod elab-mod$a))
(wires (g :wires elab-mod$a))
(insts (g :insts elab-mod$a)))
(and (modname-p name)
(natp totalwires)
(natp totalinsts)
(module-p orig-mod)
(wirelist-nodups-p wires)
(elab-modinsts-nodups-p insts)
(equal elab-mod$a
(s :name name
(s :totalwires totalwires
(s :totalinsts totalinsts
(s :orig-mod orig-mod
(s :wires
wires (s :insts insts nil)))))))))))
