• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
          • Scopestack
          • Filtering-by-name
          • Vl-namefactory
          • Substitution
          • Allexprs
          • Hid-tools
            • Following-hids
            • Vl-hidexpr-traverse-datatype
            • Abstract-hids
              • Vl-hidexpr-p
              • Vl-hidindex-p
              • Vl-hidexpr-collect-indices
              • Vl-hidindex->indices
              • Vl-hidexpr->rest
                • Vl-indexexpr->indices
                • Vl-hidexpr->first
                • Vl-indexexpr->scopeexpr
                • Vl-scopeexpr->scopes
                • Vl-hidname-p
                • Vl-hidexpr->endp
                • Vl-scopeexpr->hid
                • Vl-hidname->name
                • Vl-hidindex->name
                • Vl-hidindex-count-indices
                • Vl-scopeexpr-p
                • Vl-scopeatom->name
                • Vl-scopename-p
                • Vl-scopename-fix
                • Vl-indexexpr-p
                • Vl-fast-keyguts-p
                • Vl-scopeatom-p
                • Vl-scopenamelist
              • Vl-hidexpr-find-type
            • Vl-consteval
            • Range-tools
            • Lvalexprs
            • Hierarchy
            • Finding-by-name
            • Expr-tools
            • Expr-slicing
            • Stripping-functions
            • Stmt-tools
            • Modnamespace
            • Vl-parse-expr-from-str
            • Welltyped
            • Reordering-by-name
            • Flat-warnings
            • Genblob
            • Expr-building
            • Datatype-tools
            • Syscalls
            • Relocate
            • Expr-cleaning
            • Namemangle
            • Caremask
            • Port-tools
            • Lvalues
          • Server
          • Kit
          • Printer
          • Esim-vl
          • Well-formedness
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Abstract-hids

    Vl-hidexpr->rest

    Signature
    (vl-hidexpr->rest x) → rest
    Arguments
    x — Guard (vl-expr-p x).
    Returns
    rest — Type (and (vl-expr-p rest) (implies (and (vl-hidexpr-p x) (not (vl-hidexpr->endp x))) (vl-hidexpr-p rest))) .

    Definitions and Theorems

    Function: vl-hidexpr->rest

    (defun vl-hidexpr->rest (x)
      (declare (xargs :guard (vl-expr-p x)))
      (declare (xargs :guard (and (vl-hidexpr-p x)
                                  (not (vl-hidexpr->endp x)))))
      (let ((__function__ 'vl-hidexpr->rest))
        (declare (ignorable __function__))
        (vl-expr-fix (second (vl-nonatom->args x)))))

    Theorem: return-type-of-vl-hidexpr->rest

    (defthm return-type-of-vl-hidexpr->rest
      (b* ((rest (vl-hidexpr->rest x)))
        (and (vl-expr-p rest)
             (implies (and (vl-hidexpr-p x)
                           (not (vl-hidexpr->endp x)))
                      (vl-hidexpr-p rest))))
      :rule-classes :rewrite)

    Theorem: vl-expr-count-of-vl-hidexpr->rest

    (defthm vl-expr-count-of-vl-hidexpr->rest
      (implies (not (vl-hidexpr->endp x))
               (< (vl-expr-count (vl-hidexpr->rest x))
                  (vl-expr-count x)))
      :rule-classes :linear)

    Theorem: vl-expr-count-of-vl-hidexpr-pieces

    (defthm vl-expr-count-of-vl-hidexpr-pieces
      (implies (and (vl-hidexpr-p x)
                    (not (vl-hidexpr->endp x)))
               (< (+ (vl-expr-count (vl-hidexpr->first x))
                     (vl-expr-count (vl-hidexpr->rest x)))
                  (vl-expr-count x)))
      :rule-classes :linear)

    Theorem: vl-hidexpr->rest-of-vl-expr-fix-x

    (defthm vl-hidexpr->rest-of-vl-expr-fix-x
      (equal (vl-hidexpr->rest (vl-expr-fix x))
             (vl-hidexpr->rest x)))

    Theorem: vl-hidexpr->rest-vl-expr-equiv-congruence-on-x

    (defthm vl-hidexpr->rest-vl-expr-equiv-congruence-on-x
      (implies (vl-expr-equiv x x-equiv)
               (equal (vl-hidexpr->rest x)
                      (vl-hidexpr->rest x-equiv)))
      :rule-classes :congruence)