From 3e7a0fbadd846ecfb762ed1c38fb2bc1cbc57150 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 17 Jul 2025 18:40:30 +0200
Subject: [PATCH] doc(Grind): propagate comments in the example propagator
 There was one useful comment in one of the four branches, but none in the
 other three. This PR adds them.

---
 Manual/Grind.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Manual/Grind.lean b/Manual/Grind.lean
index 5f12dbaa..4a2c528a 100644
--- a/Manual/Grind.lean
+++ b/Manual/Grind.lean
@@ -178,19 +178,22 @@ namespace ExamplePropagators
 builtin_grind_propagator propagateAndUp ↑And := fun e => do
   let_expr And a b := e | return ()
   if (← isEqTrue a) then
-    -- a = True  ⇒  (a ∧ b) = b
+    -- a = True ⇒ (a ∧ b) = b
     pushEq e b <|
       mkApp3 (mkConst ``Grind.and_eq_of_eq_true_left)
         a b (← mkEqTrueProof a)
   else if (← isEqTrue b) then
+    -- b = True ⇒ (a ∧ b) = a
     pushEq e a <|
       mkApp3 (mkConst ``Grind.and_eq_of_eq_true_right)
         a b (← mkEqTrueProof b)
   else if (← isEqFalse a) then
+    -- a = False ⇒ (a ∧ b) = False
     pushEqFalse e <|
       mkApp3 (mkConst ``Grind.and_eq_of_eq_false_left)
         a b (← mkEqFalseProof a)
   else if (← isEqFalse b) then
+    -- b = False ⇒ (a ∧ b) = False
     pushEqFalse e <|
       mkApp3 (mkConst ``Grind.and_eq_of_eq_false_right)
         a b (← mkEqFalseProof b)