• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
          • Unparameterization
          • Elaborate
          • Addnames
          • Annotate
          • Clean-warnings
          • Eliminitial
          • Custom-transform-hooks
            • Vl-design-constcheck-hook
            • Vl-centaur-seqcheck-hook
            • Mp-verror-transform-hook
            • Problem-modules
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Custom-transform-hooks

    Mp-verror-transform-hook

    Centaur specific transform.

    Definitions and Theorems

    Theorem: vl-design-p-of-mp-verror-transform-hook

    (defthm vl-design-p-of-mp-verror-transform-hook
            (vl-design-p (mp-verror-transform-hook x)))