make the CI target the new formulation

Verified-zkEVM · Dec 18, 2024 · e51b671 · e51b671
1 parent 27268d9
commit e51b671
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/Clean.lean b/Clean.lean
@@ -1,2 +1,7 @@
-import Clean.Tables.Addition8
-import Clean.Tables.Fibonacci
+
+-- old version
+-- import Clean.Tables.Addition8
+-- import Clean.Tables.Fibonacci
+
+-- new version
+import Clean.Examples.Gadgets
diff --git a/Clean/GadgetsNew/Boolean.lean b/Clean/GadgetsNew/Boolean.lean
@@ -8,8 +8,7 @@ import Clean.Circuit.Basic
 import Clean.Utils.Field
 
 section
-variable {p : ℕ} [Fact (p ≠ 0)] [Fact p.Prime]
-variable [p_large_enough: Fact (p > 512)]
+variable {p : ℕ} [Fact p.Prime]
 
 open Circuit
 open Expression