From b7281e9fe25215998c86d6c8ea167f4a25b4c42f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Oct 2021 11:36:40 -0700 Subject: [PATCH] fix: instruct pretty printer to add a line break after each `calc` step It should fix https://github.com/leanprover/mathport/issues/26 --- src/Init/NotationExtra.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index be65fb6604..dbf41b35a1 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -95,7 +95,7 @@ macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBi -- enforce indentation of calc steps so we know when to stop parsing them syntax calcStep := colGe term " := " withPosition(term) -syntax (name := calc) "calc " withPosition(calcStep+) : term +syntax (name := calc) "calc " withPosition((calcStep ppLine)+) : term macro "calc " steps:withPosition(calcStep+) : tactic => `(exact calc $(steps.getArgs)*)