chore: expand comment

leanprover · Jan 2, 2025 · 3c0d9bf · 3c0d9bf
1 parent a127c9d
commit 3c0d9bf
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean
@@ -222,7 +222,8 @@ def rewriteRulesPass (maxSteps : Nat) : Pass where
     return newGoal
 
 /--
-Responsible for applying short-circuit optimizations for `*`.
+Responsible for applying short-circuit optimizations for `*`, e.g.,
+translating `x1 * y == x2 * y` to `!(!x1 == x2 && !x1 * y == x2 * y)`.
 -/
 def shortCircuitPass (maxSteps : Nat) : Pass where
   name := `shortCircuitPass