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)*)