Kyle Miller cd0b54ce5d feat: tag structure instances when pp.tagAppFn is set (#7840) ... This PR causes structure instance notation to be tagged with the constructor when `pp.tagAppFns` is true. This will make docgen will have `{` and `}` be links to the structure constructor.		2025-04-07 05:07:05 +00:00
..
Delaborator	feat: tag structure instances when pp.tagAppFn is set (#7840)	2025-04-07 05:07:05 +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	feat: modify delaborator to tag generalized field notation (#6703)	2025-02-02 21:34:49 +00:00
Parenthesizer.lean	feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)	2024-11-22 03:05:51 +00:00