		Search-engine friendly clone of the ACL2 documentation.

Defsvtv-args

Defsvtv-args-p

Recognizer for defsvtv-args structures.

Signature
(defsvtv-args-p x) → *

Definitions and Theorems

Function: defsvtv-args-p

(defun defsvtv-args-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'defsvtv-args-p))
    (declare (ignorable __function__))
    (and (true-listp x)
         (eql (len x) 26)
         (b* ((name (std::da-nth 0 x))
              (stages (std::da-nth 1 x))
              (inputs (std::da-nth 2 x))
              (overrides (std::da-nth 3 x))
              (outputs (std::da-nth 4 x))
              (internals (std::da-nth 5 x))
              (design (std::da-nth 6 x))
              (design-const (std::da-nth 7 x))
              (labels (std::da-nth 8 x))
              (phase-config (std::da-nth 9 x))
              (clocks (std::da-nth 10 x))
              (phase-scc-limit (std::da-nth 11 x))
              (monotonify (std::da-nth 12 x))
              (simplify (std::da-nth 13 x))
              (pre-simplify (std::da-nth 14 x))
              (pipe-simp (std::da-nth 15 x))
              (cycle-phases (std::da-nth 16 x))
              (?cycle-phases-p (std::da-nth 17 x))
              (cycle-simp (std::da-nth 18 x))
              (initial-state-vars (std::da-nth 19 x))
              (?define-macros (std::da-nth 20 x))
              (?define-mod (std::da-nth 21 x))
              (?parents (std::da-nth 22 x))
              (?short (std::da-nth 23 x))
              (?long (std::da-nth 24 x))
              (?form (std::da-nth 25 x)))
           (and (symbolp name)
                (true-list-listp stages)
                (true-list-listp inputs)
                (true-list-listp overrides)
                (true-list-listp outputs)
                (true-list-listp internals)
                (design-p design)
                (symbolp design-const)
                (symbol-listp labels)
                (phase-fsm-config-p phase-config)
                (svarlist-p clocks)
                (maybe-natp phase-scc-limit)
                (booleanp monotonify)
                (booleanp simplify)
                (booleanp pre-simplify)
                (svex-simpconfig-p pipe-simp)
                (svtv-cyclephaselist-p cycle-phases)
                (svex-simpconfig-p cycle-simp)
                (booleanp initial-state-vars))))))

Theorem: consp-when-defsvtv-args-p

(defthm consp-when-defsvtv-args-p
  (implies (defsvtv-args-p x) (consp x))
  :rule-classes :compound-recognizer)