minor

Verified-zkEVM · Dec 17, 2024 · ad4a50c · ad4a50c
1 parent 344f7e2
commit ad4a50c
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Clean/Circuit/Circuit.lean b/Clean/Circuit/Circuit.lean
@@ -614,7 +614,6 @@ def circuit : FormalCircuit (F p) (fields (F p) 3) (field (F p)) where
     rintro env ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩ h_inputs as
     let [x, y, carry_in] := inputs
     let [x_var, y_var, carry_in_var] := inputs_var
-    -- let [z, carry_out] := witnesses
     rintro h_holds z'
 
     -- characterize inputs