Leonardo de Moura 3c17755730 chore: prepare to remove coe definitions ... The notation `↑ e` will eagerly expand the coersion. See #403		2022-01-20 15:07:54 -08:00
..
Delaborator	chore: prepare to remove coe definitions	2022-01-20 15:07:54 -08:00
Basic.lean	chore: throwError! => throwError, throwErrorAt! => throwErrorAt	2021-03-11 11:59:45 -08:00
Delaborator.lean	refactor: pp.analyze needs pp options	2021-08-03 09:13:18 +02:00
Formatter.lean	fix: don't drop tags in identNoAntiquot	2022-01-03 13:43:33 +01:00
Parenthesizer.lean	chore: remove arbitrary	2022-01-15 12:14:27 -08:00