Recognize Jubjub points and
(maybe-jubjub-pointp x) → yes/no
These are optional Jubjub points. Useful, for instance, as results of functions that may return either Jubjub points or an error value.
(defun maybe-jubjub-pointp (x) (declare (xargs :guard t)) (let ((__function__ 'maybe-jubjub-pointp)) (declare (ignorable __function__)) (or (jubjub-pointp x) (eq x nil))))
(defthm booleanp-of-maybe-jubjub-pointp (b* ((yes/no (maybe-jubjub-pointp x))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm maybe-jubjub-pointp-when-jubjub-pointp (implies (jubjub-pointp x) (maybe-jubjub-pointp x)))