		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-sort-blockitems

Signature
(vl-sort-blockitems x) → (mv vardecls paramdecls imports typedefs)
Arguments: x — Guard (vl-blockitemlist-p x).
Returns: vardecls — Type (vl-vardecllist-p vardecls).; paramdecls — Type (vl-paramdecllist-p paramdecls).; imports — Type (vl-importlist-p imports).; typedefs — Type (vl-typedeflist-p typedefs).

Definitions and Theorems

Function: vl-sort-blockitems

(defun vl-sort-blockitems (x)
  (declare (xargs :guard (vl-blockitemlist-p x)))
  (let ((__function__ 'vl-sort-blockitems))
    (declare (ignorable __function__))
    (vl-sort-blockitems-aux x nil nil nil nil)))

Theorem: vl-vardecllist-p-of-vl-sort-blockitems.vardecls

(defthm vl-vardecllist-p-of-vl-sort-blockitems.vardecls
  (b* (((mv ?vardecls
            ?paramdecls ?imports ?typedefs)
        (vl-sort-blockitems x)))
    (vl-vardecllist-p vardecls))
  :rule-classes :rewrite)

Theorem: vl-paramdecllist-p-of-vl-sort-blockitems.paramdecls

(defthm vl-paramdecllist-p-of-vl-sort-blockitems.paramdecls
  (b* (((mv ?vardecls
            ?paramdecls ?imports ?typedefs)
        (vl-sort-blockitems x)))
    (vl-paramdecllist-p paramdecls))
  :rule-classes :rewrite)

Theorem: vl-importlist-p-of-vl-sort-blockitems.imports

(defthm vl-importlist-p-of-vl-sort-blockitems.imports
  (b* (((mv ?vardecls
            ?paramdecls ?imports ?typedefs)
        (vl-sort-blockitems x)))
    (vl-importlist-p imports))
  :rule-classes :rewrite)

Theorem: vl-typedeflist-p-of-vl-sort-blockitems.typedefs

(defthm vl-typedeflist-p-of-vl-sort-blockitems.typedefs
  (b* (((mv ?vardecls
            ?paramdecls ?imports ?typedefs)
        (vl-sort-blockitems x)))
    (vl-typedeflist-p typedefs))
  :rule-classes :rewrite)

Theorem: vl-sort-blockitems-of-vl-blockitemlist-fix-x

(defthm vl-sort-blockitems-of-vl-blockitemlist-fix-x
  (equal (vl-sort-blockitems (vl-blockitemlist-fix x))
         (vl-sort-blockitems x)))

Theorem: vl-sort-blockitems-vl-blockitemlist-equiv-congruence-on-x

(defthm vl-sort-blockitems-vl-blockitemlist-equiv-congruence-on-x
  (implies (vl-blockitemlist-equiv x x-equiv)
           (equal (vl-sort-blockitems x)
                  (vl-sort-blockitems x-equiv)))
  :rule-classes :congruence)