• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
          • Unparameterization
          • Elaborate
          • Addnames
          • Annotate
            • Increment-elim
            • Make-implicit-wires
            • Basic-bind-elim
              • Vl-modulelist-apply-binddelta
              • Vl-interfacelist-apply-binddelta
              • Vl-bindelim-main
              • Vl-bindelim-bindlist
              • Vl-bindelim-find-global-target
              • Vl-interfacelist-bindelim
              • Vl-modulelist-bindelim
              • Vl-interface-bindelim
              • Vl-module-bindelim
              • Vl-bindelim-institem
                • Vl-bindelim-institem-fix
                • Vl-bindelim-institem-equiv
                • Make-vl-bindelim-institem
                • Vl-bindelim-institem->inst
                • Vl-bindelim-institem->ctx
                • Vl-bindelim-institem->bindp
                • Vl-bindelim-institem->genp
                • Change-vl-bindelim-institem
                • Vl-bindelim-institem-p
                • Vl-warn-bindintentlist-undefined
                • Vl-warn-bindintent-undefined
                • Vl-interfacelist-bindelim-insttable
                • Vl-modulelist-bindelim-insttable
                • Vl-warn-binddelta-undefined
                • Vl-interface-bindelim-insttable
                • Vl-interface-apply-binddelta
                • Vl-design-bindelim-pass2
                • Vl-bindelim-modinstlist-add-atts
                • Vl-module-bindelim-insttable
                • Vl-module-apply-binddelta
                • Vl-bindelim-modinst-add-atts
                • Vl-design-bindelim-pass1
                • Vl-bindcontext
                • Vl-bindintent->modinsts
                • Vl-bindelim-insttable
                • Vl-bindintentlist->modinsts
                • Vl-binddelta
                • Vl-design-bindelim
                • Vl-bindelim-institemlist
              • Argresolve
              • Basicsanity
              • Portdecl-sign
              • Enum-names
              • Port-resolve
              • Udp-elim
              • Vl-annotate-design
              • Vl-annotate-module
            • Clean-warnings
            • Eliminitial
            • Custom-transform-hooks
            • Problem-modules
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-bindelim-institem

    Vl-bindelim-institem-p

    Recognizer for vl-bindelim-institem structures.

    Signature
    (vl-bindelim-institem-p x) → *

    Definitions and Theorems

    Function: vl-bindelim-institem-p

    (defun vl-bindelim-institem-p (x)
      (declare (xargs :guard t))
      (let ((__function__ 'vl-bindelim-institem-p))
        (declare (ignorable __function__))
        (and (std::prod-consp x)
             (std::prod-consp (std::prod-car x))
             (std::prod-consp (std::prod-cdr x))
             (b* ((inst (std::prod-car (std::prod-car x)))
                  (genp (std::prod-cdr (std::prod-car x)))
                  (bindp (std::prod-car (std::prod-cdr x)))
                  (ctx (std::prod-cdr (std::prod-cdr x))))
               (and (vl-modinst-p inst)
                    (booleanp genp)
                    (booleanp bindp)
                    (vl-bindcontext-p ctx))))))