• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Defresult
      • Deffixtype
      • Deffixequiv
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Defset
      • Fty::basetypes
        • Any-p
        • Symbol-fix
        • Maybe-integerp-fix
        • Maybe-natp-fix
        • Maybe-integer-equiv
        • Maybe-posp-fix
        • Maybe-pos-equiv
        • Maybe-nat-equiv
        • Maybe-bit-fix
        • Maybe-bit-equiv
        • Bool-fix
        • Symbol-equiv
        • Maybe-lit-fix
        • True-equiv
        • Pos-equiv
        • Lposfix
        • True-p
        • True-fix
      • Specific-types
      • Defvisitors
      • Deffixtype-alias
      • Defomap
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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))