		Search-engine friendly clone of the ACL2 documentation.

Dupeinst-check

Vl-dupeinst-trivial-p

Customizable filter for duplicate module instances.

By default, all duplicated modules are considered worth warning about. But you can configure which modules are considered trivial/okay to duplicate by attaching a function to vl-dupeinst-trivial-p. These will be filtered out into minor warnings.

Definition: vl-dupeinst-trivial-p

(encapsulate (((vl-dupeinst-trivial-p *)
               => *
               :formals (modname)
               :guard (stringp modname)))
  (local (value-triple :elided)))

Definitions and Theorems

Function: vl-dupeinst-trivial-p-default

(defun vl-dupeinst-trivial-p-default (modname)
  (declare (xargs :guard (stringp modname))
           (ignore modname))
  nil)