maybe-natp

(in-package "ACL2")

(defsection maybe-natp
  :parents (natp std/basic)
  :short "Recognizer for naturals and @('nil')."
  :long "<p>This is like an <a
href='https://en.wikipedia.org/wiki/Option_type'>option type</a>; when @('x')
satisfies @('maybe-natp'), then either it is a natural number or nothing.</p>"
  (defund-inline maybe-natp
    (x)
    (declare (xargs :guard t))
    (or (not x) (natp x)))
  (local (in-theory (enable maybe-natp)))
  (defthm maybe-natp-compound-recognizer
    (equal (maybe-natp x)
      (or (not x) (and (integerp x) (<= 0 x))))
    :rule-classes :compound-recognizer))