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

feat: add calc tactic macro

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-30 09:33:32 -07:00
parent ce47000e33
commit f4c72025ee
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/NotationExtra.lean
View file

@ -101,6 +101,8 @@ macro_rules
| `(calc $p:term := $h:term) => `(show $p from $h)
| `(calc $p:term := $h:term $rest:calcStep*) => ``(trans (show $p from $h) (calc $rest:calcStep*))
macro "calc " steps:withPosition(calcStep+) : tactic => `(exact calc $(steps.getArgs)*)
@[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
| `($(_)) => `(())
| _ => throw ()