Cameron Zwarich 632b688cb7 feat: add an LCNF pass to convert structure projections to cases expressions (#8367) ... This PR adds a new `structProjCases` pass to the new compiler, analogous to the `struct_cases_on` pass in the old compiler, which converts all projections from structs into `cases` expressions. When lowered to IR, this causes all of the projections from a single structure to be grouped together, which is an invariant relied upon by the IR RC passes (at least for linearity, if not general correctness).		2025-05-15 21:54:25 +00:00
..
Compiler	feat: add an LCNF pass to convert structure projections to cases expressions (#8367)	2025-05-15 21:54:25 +00:00
Data	fix: exponential compilation times due to inlined instances (#8254)	2025-05-07 08:27:14 +00:00
DocString	feat: move non-essential metadata into .olean.server (#8068)	2025-04-24 08:12:26 +00:00
Elab	fix: cases tactic to handle non-atomic eliminator well (#8361)	2025-05-15 16:59:11 +00:00
Language	feat: do not export def bodies by default (#8221)	2025-05-15 12:16:54 +00:00
Linter	feat: implement "linter sets" that can be turned on as a group (#8106)	2025-05-14 23:30:42 +00:00
Meta	fix: use withReducibleAndIntances to match ground patterns (#8365)	2025-05-15 19:50:46 +00:00
Parser	feat: do not export def bodies by default (#8221)	2025-05-15 12:16:54 +00:00
ParserCompiler
PrettyPrinter	feat: add labeled subcomponents and helper functions for error messages (#8225)	2025-05-07 21:15:27 +00:00
Server	feat: do not export def bodies by default (#8221)	2025-05-15 12:16:54 +00:00
Util	feat: lean --setup (#8024)	2025-05-03 23:57:37 +00:00
Widget	chore: remove old documentation site (#7974)	2025-05-14 14:31:33 +00:00
AddDecl.lean	feat: do not export def bodies by default (#8221)	2025-05-15 12:16:54 +00:00
Attributes.lean
AuxRecursor.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
BuiltinDocAttr.lean
Class.lean
Compiler.lean
CoreM.lean	feat: LCNF -> IR translation (#8211)	2025-05-03 05:34:37 +00:00
Data.lean	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
Declaration.lean	feat: do not export theorem bodies (#8090)	2025-04-25 20:22:32 +00:00
DeclarationRange.lean	feat: move non-essential metadata into .olean.server (#8068)	2025-04-24 08:12:26 +00:00
DocString.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
Elab.lean
EnvExtension.lean	feat: move non-essential metadata into .olean.server (#8068)	2025-04-24 08:12:26 +00:00
Environment.lean	feat: do not export def bodies by default (#8221)	2025-05-15 12:16:54 +00:00
Exception.lean	feat: 'unknown identifier' code actions (#7665)	2025-04-02 09:43:40 +00:00
Expr.lean	fix: grind +splitImp, arrow propagator, missing normalization rule (#8158)	2025-04-28 22:59:43 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean
Level.lean	chore: do not use the coercion α → Option α in Init and Std (#8085)	2025-04-24 13:35:01 +00:00
Linter.lean	feat: implement "linter sets" that can be turned on as a group (#8106)	2025-05-14 23:30:42 +00:00
LoadDynlib.lean
LocalContext.lean
Log.lean
Message.lean	feat: guard_msgs to treat trace messages separate (#8267)	2025-05-09 05:44:34 +00:00
Meta.lean	feat: add labeled subcomponents and helper functions for error messages (#8225)	2025-05-07 21:15:27 +00:00
MetavarContext.lean	doc: fix typo in MetavarDecl docstring (#8069)	2025-04-23 22:00:13 +00:00
Modifiers.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
MonadEnv.lean	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
Namespace.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
Parser.lean
ParserCompiler.lean
PremiseSelection.lean
PrettyPrinter.lean	fix: don't reset localInstances in delaboration (#8022)	2025-04-19 15:39:16 +00:00
PrivateName.lean	chore: do not use the coercion α → Option α in Init and Std (#8085)	2025-04-24 13:35:01 +00:00
ProjFns.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
ReducibilityAttrs.lean
Replay.lean
ReservedNameAction.lean	feat: elaborate theorem bodies in parallel (#7084)	2025-03-14 07:50:42 +00:00
ResolveName.lean	perf: use isReservedName in Environment.findAsync?	2025-03-25 17:22:22 +01:00
Runtime.lean
ScopedEnvExtension.lean
Server.lean
Setup.lean	chore: fix spelling mistakes (#8324)	2025-05-14 06:52:16 +00:00
Structure.lean	refactor: factor out common code for structure default values (#7737)	2025-03-31 22:40:39 +00:00
SubExpr.lean
Syntax.lean	chore: do not use the coercion α → Option α in Init and Std (#8085)	2025-04-24 13:35:01 +00:00
ToExpr.lean
ToLevel.lean
Util.lean
Widget.lean