From e826f5f42a52c9865bacd8b7dd2e89c2698d2d94 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 2 Jun 2023 01:30:48 -0400
Subject: [PATCH] fix: spacing around `calc`

---
 src/Init/NotationExtra.lean             | 2 +-
 tests/lean/formatTerm.lean              | 4 ++++
 tests/lean/formatTerm.lean.expected.out | 3 +++
 3 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 6be1cb0f12..1b7a8296e8 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -92,7 +92,7 @@ end
 syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
 -- enforce indentation of calc steps so we know when to stop parsing them
 syntax calcStep := ppIndent(colGe term " := " term)
-syntax calcSteps := ppLine withPosition(calcFirstStep) ppLine withPosition((calcStep ppLine)*)
+syntax calcSteps := ppLine withPosition(calcFirstStep) withPosition((ppLine calcStep)*)
 
 /-- Step-wise reasoning over transitive relations.
 ```
diff --git a/tests/lean/formatTerm.lean b/tests/lean/formatTerm.lean
index 1500e469b4..b8c9dfea54 100644
--- a/tests/lean/formatTerm.lean
+++ b/tests/lean/formatTerm.lean
@@ -59,3 +59,7 @@ def foo : a b c d e f g a b c d e f g h where
   i := 42
   j := 42
   k := 42)
+
+#eval fmt `(calc
+  1 = 1 := rfl
+  1 = 1 := rfl)
diff --git a/tests/lean/formatTerm.lean.expected.out b/tests/lean/formatTerm.lean.expected.out
index 70ede97f22..0928ad1263 100644
--- a/tests/lean/formatTerm.lean.expected.out
+++ b/tests/lean/formatTerm.lean.expected.out
@@ -67,3 +67,6 @@ def foo✝ : a✝ b✝ c✝ d✝ e✝ f✝ g✝ a✝ b✝ c✝ d✝ e✝ f✝ g
   i✝ := 42
   j✝ := 42
   k✝ := 42
+calc
+  1 = 1 := rfl✝
+  1 = 1 := rfl✝