Recognizer for curve.
(curvep x) → fty::yes/no
Function: curvep
(defun curvep (x) (declare (xargs :guard t)) (eq x :edwards-bls12))
Theorem: booleanp-of-curvep
(defthm booleanp-of-curvep (b* ((fty::yes/no (curvep x))) (booleanp fty::yes/no)) :rule-classes :rewrite)