Leonardo de Moura b1e52f1475 chore: mark Meta.Context.config as private (#6051) ... Motivation: we want to modify the internal representation and improve `isDefEq` caching. This PR is preparing the stage for future modifications.		2024-11-13 13:30:06 +11:00
..
Attributes.lean	feat: add pp.fieldNotation.generalized for generalized field notation, add @[pp_nodot] attribute (#3737)	2024-03-22 08:55:02 +00:00
Basic.lean	feat: accurate binder names in signatures (like in output of #check) (#5827)	2024-10-29 16:43:11 +00:00
Builtins.lean	fix: avoid delaborating with field notation if object is a metavariable (#6014)	2024-11-08 20:57:37 +00:00
FieldNotation.lean	fix: check is valid structure projection when pretty printing (#4982)	2024-08-12 15:52:17 +00:00
Options.lean	feat: options pp.mvars.anonymous and pp.mvars.levels (#5711)	2024-10-14 21:44:15 +00:00
SubExpr.lean	feat: accurate binder names in signatures (like in output of #check) (#5827)	2024-10-29 16:43:11 +00:00
TopDownAnalyze.lean	chore: mark Meta.Context.config as private (#6051)	2024-11-13 13:30:06 +11:00