• 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
          • Lint-warning-suppression
          • Warning-basics
          • Vl-warning
            • Vl-warning-p
            • Vl-warning-fix
            • Make-vl-warning
            • Vl-warning-equiv
            • Change-vl-warning
            • Vl-warning->suppressedp
            • Vl-warning->type
            • Vl-warning->fatalp
              • Vl-warning->args
              • Vl-warning->msg
              • Vl-warning->fn
              • Vl-warning->context
            • Vl-warninglist-add-ctx
            • Vl-warninglist->types
            • Propagating-errors
            • Vl-reportcard
            • Vl-some-warning-fatalp
            • Clean-warnings
            • Lint-whole-file-suppression
            • Warn
            • Vl-warninglist
            • Vl-remove-warnings
            • Vl-keep-warnings
            • Flat-warnings
            • Vl-some-warning-of-type-p
            • Vl-msg
            • Vl-warning-add-ctx
            • Vl-print-warning
            • Vmsg-binary-concat
            • Ok
            • Vl-trace-warnings
            • Fatal
            • Vmsg
          • Getting-started
          • Utilities
          • Printer
          • Kit
          • Mlib
          • Transforms
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-warning

    Vl-warning->fatalp

    Get the fatalp field from a vl-warning.

    Signature
    (vl-warning->fatalp x) → fatalp
    Arguments
    x — Guard (vl-warning-p x).
    Returns
    fatalp — Type (booleanp fatalp).

    This is an ordinary field accessor created by defprod.

    Definitions and Theorems

    Function: vl-warning->fatalp$inline

    (defun vl-warning->fatalp$inline (x)
      (declare (xargs :guard (vl-warning-p x)))
      (declare (xargs :guard t))
      (let ((__function__ 'vl-warning->fatalp))
        (declare (ignorable __function__))
        (mbe :logic
             (b* ((x (and t x)))
               (acl2::bool-fix (cdr (std::da-nth 4 (cdr x)))))
             :exec (cdr (std::da-nth 4 (cdr x))))))

    Theorem: booleanp-of-vl-warning->fatalp

    (defthm booleanp-of-vl-warning->fatalp
      (b* ((fatalp (vl-warning->fatalp$inline x)))
        (booleanp fatalp))
      :rule-classes :type-prescription)

    Theorem: vl-warning->fatalp$inline-of-vl-warning-fix-x

    (defthm vl-warning->fatalp$inline-of-vl-warning-fix-x
      (equal (vl-warning->fatalp$inline (vl-warning-fix x))
             (vl-warning->fatalp$inline x)))

    Theorem: vl-warning->fatalp$inline-vl-warning-equiv-congruence-on-x

    (defthm vl-warning->fatalp$inline-vl-warning-equiv-congruence-on-x
      (implies (vl-warning-equiv x x-equiv)
               (equal (vl-warning->fatalp$inline x)
                      (vl-warning->fatalp$inline x-equiv)))
      :rule-classes :congruence)