		Search-engine friendly clone of the ACL2 documentation.

Curve-fix

Fixer for curve.

Function: curve-fix

(defun curve-fix (x)
  (declare (xargs :guard (curvep x)))
  (mbe :logic (if (curvep x) x :edwards-bls12)
       :exec x))

Theorem: curvep-of-curve-fix

(defthm curvep-of-curve-fix
  (b* ((fixed-x (curve-fix x)))
    (curvep fixed-x))
  :rule-classes :rewrite)

Theorem: curve-fix-when-curvep

(defthm curve-fix-when-curvep
  (implies (curvep x)
           (equal (curve-fix x) x)))