From e3a8d132bef7ba261b19292ef76011251165c567 Mon Sep 17 00:00:00 2001 From: martyall Date: Wed, 9 Sep 2026 22:27:56 -0700 Subject: [PATCH] Curves/Pasta: thunk fintypePoints so compiled binaries do not evaluate it at startup --- CompElliptic/Curves/Pasta.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CompElliptic/Curves/Pasta.lean b/CompElliptic/Curves/Pasta.lean index 0bc3185..6d70f1c 100644 --- a/CompElliptic/Curves/Pasta.lean +++ b/CompElliptic/Curves/Pasta.lean @@ -113,7 +113,7 @@ example (P : SWPoint curve) : (-1 : ℤ) • P = -P := neg_one_zsmul P /-- The Pallas point enumeration, as a computable instantiation of `instFintypeSWPoint`: the filter of `F × F` by the decidable `Valid` predicate. Named so the trust census can pin its computability. -/ -abbrev fintypePoints : Fintype (SWPoint curve) := inferInstance +abbrev fintypePoints (_ : Unit) : Fintype (SWPoint curve) := inferInstance end Pallas @@ -198,7 +198,7 @@ example : OnCurve a b (smul a 3 G) := by native_decide /-- The Vesta point enumeration, as a computable instantiation of `instFintypeSWPoint`: the filter of `F × F` by the decidable `Valid` predicate. Named so the trust census can pin its computability. -/ -abbrev fintypePoints : Fintype (SWPoint curve) := inferInstance +abbrev fintypePoints (_ : Unit) : Fintype (SWPoint curve) := inferInstance end Vesta