From 35e8e6e903eb0af55e2c84ed3907442a9397e087 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Wed, 29 Nov 2023 17:48:01 +0000
Subject: [PATCH] Added N as argument

---
 ProvenZk/Gates.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean
index 7409c24..29c644e 100644
--- a/ProvenZk/Gates.lean
+++ b/ProvenZk/Gates.lean
@@ -81,7 +81,7 @@ structure Gates_base (α : Type) : Type where
   to_binary : α → (n : Nat) → Vector α n → Prop
   from_binary : Vector α d → α → Prop
 
-def GatesGnark_8 {N : Nat} [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
+def GatesGnark_8 (N : Nat) [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
   is_bool := GatesDef.is_bool,
   add := GatesDef.add,
   mul_acc := GatesDef.mul_acc,
@@ -105,6 +105,6 @@ def GatesGnark_8 {N : Nat} [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
   from_binary := GatesDef.from_binary
 }
 
-def GatesGnark_9 {N : Nat} [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
-  GatesGnark_8 with cmp := GatesDef.cmp_9
+def GatesGnark_9 (N : Nat) [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
+  GatesGnark_8 N with cmp := GatesDef.cmp_9
 }