lean4-htt/src/Init
Leonardo de Moura 8c6f536367 chore: avoid fun | ... => notation
@Kha the pretty printer fails when we use the `fun+match` macro. Example:
```
fun
 | PSum.inl a => 1 + sizeof a
 | PSum.inr b => 1 + sizeof b
```
The test `Reparen.lean` fails without this commit. Here is the error message
```
error: no known parenthesizer for kind 'Lean.Parser.Term.matchAlts'
```
2020-10-25 09:36:44 -07:00
..
Control chore: move to new frontend 2020-10-23 16:13:55 -07:00
Data chore: move Core.lean to new frontend 2020-10-25 08:54:37 -07:00
System chore: move to new frontend 2020-10-23 16:56:36 -07:00
Coe.lean chore: remove old HasCoe 2020-10-24 16:22:52 -07:00
Control.lean chore: move to new frontend 2020-10-23 16:35:46 -07:00
Core.lean chore: avoid fun | ... => notation 2020-10-25 09:36:44 -07:00
Data.lean chore: move to new frontend 2020-10-23 16:35:46 -07:00
Fix.lean chore: move to new frontend 2020-10-23 16:35:46 -07:00
LeanInit.lean feat: add helper functions for writing macros 2020-10-23 10:59:59 -07:00
System.lean chore: move to new frontend 2020-10-23 16:35:46 -07:00
Util.lean chore: move to new frontend 2020-10-23 12:50:03 -07:00
WF.lean chore: move to new frontend 2020-10-23 19:59:46 -07:00