• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
        • Maybe-stringp
        • Maybe-natp
          • Maybe-natp-fix
            • Maybe-nat-equiv
          • Two-nats-measure
          • Impossible
          • Bytep
          • Nat-list-measure
          • Maybe-posp
          • Nibblep
          • Organize-symbols-by-pkg
          • Organize-symbols-by-name
          • Lnfix
          • Good-valuep
          • Streqv
          • Chareqv
          • Symbol-package-name-non-cl
          • Arith-equivs
          • Induction-schemes
          • Maybe-integerp
          • Char-fix
          • Pos-fix
          • Symbol-package-name-lst
          • Mbt$
          • Maybe-bitp
          • Good-pseudo-termp
          • Str-fix
          • Maybe-string-fix
          • Nonkeyword-listp
          • Lifix
          • Bfix
          • Std/basic/if*
          • Impliez
          • Tuplep
          • Std/basic/intern-in-package-of-symbol
          • Lbfix
          • Std/basic/symbol-name-lst
          • True
          • Std/basic/rfix
          • Std/basic/realfix
          • Std/basic/member-symbol-name
          • Std/basic/fix
          • False
          • Std/basic/nfix
          • Std/basic/ifix
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Fty::basetypes
    • Maybe-natp

    Maybe-natp-fix

    (maybe-natp-fix x) is the identity for maybe-natps, or coerces any invalid object to nil.

    Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.

    Definitions and Theorems

    Function: maybe-natp-fix$inline

    (defun maybe-natp-fix$inline (x)
  (declare (xargs :guard (maybe-natp x)))
  (mbe :logic (if x (nfix x) nil)
       :exec x))

    Theorem: maybe-natp-of-maybe-natp-fix

    (defthm maybe-natp-of-maybe-natp-fix
  (maybe-natp (maybe-natp-fix x))
  :rule-classes (:rewrite :type-prescription))

    Theorem: maybe-natp-fix-when-maybe-natp

    (defthm maybe-natp-fix-when-maybe-natp
  (implies (maybe-natp x)
           (equal (maybe-natp-fix x) x)))

    Theorem: maybe-natp-fix-under-iff

    (defthm maybe-natp-fix-under-iff
  (iff (maybe-natp-fix x) x))

    Theorem: maybe-natp-fix-under-nat-equiv

    (defthm maybe-natp-fix-under-nat-equiv
  (nat-equiv (maybe-natp-fix x) x))