Cameron Zwarich 3aa479fd8c fix: cache TrivialStructureInfo in LCNF toMono (#8758) ... This PR adds caching for the `hasTrivialStructure?` function for LCNF types. This is one of the hottest small functions in the new compiler, so adding a cache makes a lot of sense.		2025-06-13 01:07:38 +00:00
..
Compiler	fix: cache TrivialStructureInfo in LCNF toMono (#8758)	2025-06-13 01:07:38 +00:00
Data	feat: server-side for module hierarchy (#8654)	2025-06-11 08:02:18 +00:00
DocString	feat: pre-stage0 groundwork for named error messages (#8649)	2025-06-11 14:52:08 +00:00
Elab	fix: refine how simp tracks unfolded local definitions (#8753)	2025-06-13 00:57:57 +00:00
Language	feat: meta phase restrictions	2025-06-12 16:36:08 +02:00
Linter	chore: fix spelling mistakes (#8711)	2025-06-10 20:24:28 +00:00
Meta	fix: refine how simp tracks unfolded local definitions (#8753)	2025-06-13 00:57:57 +00:00
Parser	feat: pre-stage0 groundwork for named error messages (#8649)	2025-06-11 14:52:08 +00:00
ParserCompiler
PrettyPrinter	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Server	feat: server-side for module hierarchy (#8654)	2025-06-11 08:02:18 +00:00
Util	feat: lake: use lean --setup (#8447)	2025-06-08 17:42:45 +00:00
Widget	feat: pre-stage0 groundwork for named error messages (#8649)	2025-06-11 14:52:08 +00:00
AddDecl.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
Attributes.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
AuxRecursor.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
BuiltinDocAttr.lean	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Class.lean	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Compiler.lean	feat: meta phase restrictions	2025-06-12 16:36:08 +02:00
CoreM.lean	feat: create private aux decls in private contexts	2025-06-03 15:53:05 +02:00
Data.lean	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
Declaration.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
DeclarationRange.lean	refactor: environment extension state splitting (#8653)	2025-06-11 12:52:04 +00:00
DefEqAttrib.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +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	refactor: environment extension state splitting (#8653)	2025-06-11 12:52:04 +00:00
Environment.lean	feat: meta phase restrictions	2025-06-12 16:36:08 +02:00
ErrorExplanation.lean	feat: pre-stage0 groundwork for error explanations (#8651)	2025-06-11 14:51:44 +00:00
Exception.lean	feat: pre-stage0 groundwork for named error messages (#8649)	2025-06-11 14:52:08 +00:00
Expr.lean	feat: diseq splitting and non-chronological backtracking for linarith (#8733)	2025-06-12 02:49:35 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean
Level.lean	fix: block adversarial exploit of non-aborting assert! (#8559)	2025-05-31 00:08:30 +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	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
Log.lean	feat: pre-stage0 groundwork for named error messages (#8649)	2025-06-11 14:52:08 +00:00
Message.lean	feat: pre-stage0 groundwork for named error messages (#8649)	2025-06-11 14:52:08 +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	feat: meta phase restrictions	2025-06-12 16:36:08 +02: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	feat: add async support to more extensions and constructions (#7363)	2025-03-06 14:27:45 +00:00
Replay.lean	chore: Mathlib fixes (#7327)	2025-03-04 13:41:30 +00:00
ReservedNameAction.lean	feat: make equational theorems of non-exposed defs private (#8519)	2025-06-04 11:52:08 +00:00
ResolveName.lean	fix: let private names be unresolved in the pretty printer, fix shadowing bug when pp.universes is true (#8617)	2025-06-03 23:37:35 +00:00
Runtime.lean
ScopedEnvExtension.lean	feat: make more constructions async-compatible (#7384)	2025-03-10 09:56:30 +00:00
Server.lean
Setup.lean	chore: fix spelling mistakes (#8711)	2025-06-10 20:24:28 +00:00
Structure.lean	refactor: factor out common code for structure default values (#7737)	2025-03-31 22:40:39 +00:00
SubExpr.lean	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
Syntax.lean	fix: replace bad simp lemmas for Id (#7352)	2025-05-22 22:45:35 +00:00
ToExpr.lean	feat: ToExpr IntX (#7268)	2025-02-28 09:32:30 +00:00
ToLevel.lean
Util.lean
Widget.lean