max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: instruct pretty printer to add a line break after each calc step

Browse source 
It should fix https://github.com/leanprover/mathport/issues/26
This commit is contained in:
Leonardo de Moura 2021-10-02 11:36:40 -07:00
parent e1f591ba61
commit b7281e9fe2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/NotationExtra.lean
View file

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