maybe-pseudo-event-formp

(in-package "ACL2")

(define maybe-pseudo-event-formp
  (x)
  :returns (yes/no booleanp)
  :parents (std/system)
  :short "Recognize @(tsee pseudo-event-formp) values and @('nil')."
  (or (pseudo-event-formp x) (null x))
  ///
  (defthm maybe-pseudo-event-formp-when-pseudo-event-formp
    (implies (pseudo-event-formp x)
      (maybe-pseudo-event-formp x))))