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