lean4-htt/src/Lean/PrettyPrinter/Delaborator
Sebastian Ullrich 8c8a6021af
perf: use constant macro scope in elabArrow (#10048)
Shrinks .olean size by avoiding variation in this very frequent but
mostly unused name
2025-08-22 11:16:05 +00:00
..
Attributes.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Basic.lean perf: use constant macro scope in elabArrow (#10048) 2025-08-22 11:16:05 +00:00
Builtins.lean fix: panic in delabPRange (#9920) 2025-08-15 01:50:23 +00:00
FieldNotation.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Options.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
SubExpr.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
TopDownAnalyze.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00