Tony Beta Lambda 99031695bd feat: display coercions with a type ascription (#6119) ... This PR adds a new delab option `pp.coercions.types` which, when enabled, will display all coercions with an explicit type ascription. [Link to Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/Roundtripping.20delaboration.20involving.20coercions) Towards #4315		2024-11-21 23:02:47 +00:00
..
Delaborator	feat: display coercions with a type ascription (#6119)	2024-11-21 23:02:47 +00:00
Basic.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Delaborator.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Formatter.lean	chore: rename Array.back to back! (#5897)	2024-10-31 09:18:18 +00:00
Parenthesizer.lean	feat: pp.parens option to pretty print with all parentheses (#2934)	2024-11-15 19:11:54 +00:00