Sebastian Ullrich b5f191724d chore: stop taking constants from kernel env in synchronous case as well (#7915) ... Makes the elaborator constant map truly independent of the kernel's in preparation for the module system where declarations in the elab env may in fact differ from the kernel env.		2025-04-20 17:56:14 +00:00
..
Compiler	fix: correctly handle extern functions in the IR elim_dead_branches pass (#8017)	2025-04-18 17:28:32 +00:00
Data	feat: universe polymorphic RArray (#8014)	2025-04-18 02:18:10 +00:00
DocString	chore: enable build-specific documentation roots (#7455)	2025-03-31 09:01:35 +00:00
Elab	chore: allow RArray to be universe polymorphic (#8013)	2025-04-18 01:10:44 +00:00
Language	fix: cancellation of synchronous part of previous elaboration (#7882)	2025-04-10 11:43:41 +00:00
Linter	feat: deprecate Array.mkArray in favour of Array.replicate	2025-03-24 08:25:00 +01:00
Meta	feat: unsat comm ring equations in grind (#8032)	2025-04-20 17:26:46 +00:00
Parser	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
ParserCompiler
PrettyPrinter	fix: remove infinite loop in withFnRefWhenTagAppFns (#7904)	2025-04-10 17:16:29 +00:00
Server	refactor: more complete channel implementation for Std.Channel (#7819)	2025-04-12 21:02:24 +00:00
Util	fix: search path related bugs (#7873)	2025-04-09 15:37:49 +00:00
Widget	fix: sorry in Infoview shouldn't show module name (#7813)	2025-04-10 21:47:07 +00:00
AddDecl.lean	chore: stop taking constants from kernel env in synchronous case as well (#7915)	2025-04-20 17:56:14 +00:00
Attributes.lean	feat: realizeConst for match equations (#7247)	2025-03-03 17:18:29 +00:00
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	doc: add docstrings to mkFreshUserName etc (#7947)	2025-04-14 04:17:45 +00:00
Data.lean	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
Declaration.lean	fix: never transfer constants from checked environment into elab branches (#7306)	2025-03-05 17:12:27 +00:00
DeclarationRange.lean	fix: find realizations from other env branches (#7385)	2025-03-10 18:04:38 +00:00
DocString.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
Elab.lean	feat: #info_trees in command (#6964)	2025-02-06 03:11:53 +00:00
EnvExtension.lean	feat: environment extension data can be split into .olean.server (#7914)	2025-04-11 13:06:19 +00:00
Environment.lean	chore: stop taking constants from kernel env in synchronous case as well (#7915)	2025-04-20 17:56:14 +00:00
Exception.lean	feat: 'unknown identifier' code actions (#7665)	2025-04-02 09:43:40 +00:00
Expr.lean	feat: structure parameter binder kind overrides (#7742)	2025-03-31 03:54:03 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean
Level.lean	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
Linter.lean	chore: fix variable names in List lemmas (#6953)	2025-02-05 09:49:14 +00:00
LoadDynlib.lean	feat: smarter plugin loading (#7090)	2025-02-18 23:03:52 +00:00
LocalContext.lean	fix: move auxDeclToFullName to LocalContext to fix name (un)resolution (#7075)	2025-03-03 16:10:54 +00:00
Log.lean	feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366)	2025-03-07 13:50:56 +00:00
Message.lean	chore: avoid unnecessary quotations in cutsat traces and counterexamples (#7877)	2025-04-08 21:01:07 +00:00
Meta.lean	feat: binderNameHint (#6947)	2025-02-06 11:03:27 +00:00
MetavarContext.lean	fix: move auxDeclToFullName to LocalContext to fix name (un)resolution (#7075)	2025-03-03 16:10:54 +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	feat: rename List.enum(From) to List.zipIdx, and Array/Vector.zipWithIndex to zipIdx (#6800)	2025-01-28 23:34:30 +00:00
PremiseSelection.lean	feat: premise selection API (#7061)	2025-02-14 04:08:18 +00:00
PrettyPrinter.lean	fix: don't reset localInstances in delaboration (#8022)	2025-04-19 15:39:16 +00:00
PrivateName.lean
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: 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	feat: make more constructions async-compatible (#7384)	2025-03-10 09:56:30 +00:00
Server.lean	fix: do not cancel async elaboration tasks (#7175)	2025-02-21 17:24:36 +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	feat: deprecate Array.mkArray in favour of Array.replicate	2025-03-24 08:25:00 +01:00
ToExpr.lean	feat: ToExpr IntX (#7268)	2025-02-28 09:32:30 +00:00
ToLevel.lean
Util.lean	feat: simp +arith sorts linear atoms (#7040)	2025-02-11 23:37:30 +00:00
Widget.lean