Remove a comment that doesn't make sense anymore

PiperOrigin-RevId: 585597252 Change-Id: Ic2ee764cb7c20a0c26ca669f4728ecfa8c6f5ef5
google-deepmind · Nov 27, 2023 · d9ca51a · d9ca51a
1 parent 977d716
commit d9ca51a
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Debate/Protocol.lean b/Debate/Protocol.lean
@@ -90,8 +90,7 @@ def bob (c s q : ℝ) : Bob := bob' c s q BobId
     We reuse Honest Bob with a weaker error probability, which we will set later. -/
 def vera (s v q : ℝ) : Vera := bob' s v q VeraId
 
-/-- One step of the debate protocol.
-    c and s are the completeness and soundness parameters of the verifier. -/
+/-- One step of the debate protocol -/
 def step (alice : Alice) (bob : Bob) (vera : Vera) (y : Vector Bool n) :
     Comp AllIds (State (n+1)) := do
   let p ← (alice _ y).allow_all