Skip to content

Commit db23cc2

Browse files
committed
stdlib: register Stdlib.EmbeddedCurveOps.Bn254 in the library root
The module was never imported by `Stdlib.Stdlib`, so CI never elaborated it. Registering it surfaced one bitrot fix: Mathlib's `WeierstrassCurve.Affine.Point.some` now takes `x y` explicitly.
1 parent 5c3374e commit db23cc2

2 files changed

Lines changed: 2 additions & 1 deletion

File tree

stdlib/lampe/Stdlib/EmbeddedCurveOps/Bn254.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ private theorem bn254_generator_nonsingular :
2727
/-- The Grumpkin generator as a Mathlib `WeierstrassCurve.Affine.Point`
2828
over the BN254 scalar field. -/
2929
def generatorPoint : (affineCurve Bn254.prime).Point :=
30-
.some bn254_generator_nonsingular
30+
.some _ _ bn254_generator_nonsingular
3131

3232
@[simp] theorem generator_eq_encodeCurvePoint :
3333
(Lampe.Stdlib.EmbeddedCurveOps.Point.generator

stdlib/lampe/Stdlib/Stdlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ import Stdlib.Compat
1111
import Stdlib.Convert
1212
import Stdlib.Default
1313
import Stdlib.EmbeddedCurveOps
14+
import Stdlib.EmbeddedCurveOps.Bn254
1415
import Stdlib.Extra
1516
import Stdlib.Field
1617
import Stdlib.Field.Bn254

0 commit comments

Comments
 (0)