Kyle Miller 414ba28cef fix: make pretty printed structure instances hoverable (#7648) ... This PR fixes a bug introduced in #7589, causing pretty printed structure instances to not be hoverable in the Infoview. This was caused by a choice node being introduced, since `{ $fields,* }` is ambiguous syntax.		2025-03-23 19:36:13 +00:00
..
Compiler	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
Data	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
DocString	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
Elab	perf: add a cache to bv_decide's reflection procedure (#7644)	2025-03-23 13:56:00 +00:00
Language	perf: avoid contended access to IO.Ref in isTracingEnabledFor (#7601)	2025-03-21 12:07:25 +00:00
Linter	fix: make List/Array modify argument order consistent (#7516)	2025-03-17 04:36:05 +00:00
Meta	feat: model-based theory combination in grind (#7641)	2025-03-23 04:06:09 +00:00
Parser	doc: docstring review for monads and transformers (#7548)	2025-03-20 12:18:46 +00:00
ParserCompiler
PrettyPrinter	fix: make pretty printed structure instances hoverable (#7648)	2025-03-23 19:36:13 +00:00
Server	chore: bump server version to 0.3.0 (#7624)	2025-03-21 12:56:59 +00:00
Util	perf: avoid contended access to IO.Ref in isTracingEnabledFor (#7601)	2025-03-21 12:07:25 +00:00
Widget	feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366)	2025-03-07 13:50:56 +00:00
AddDecl.lean	fix: avoid follow-up kernel errors (#7570)	2025-03-20 09:11:25 +00:00
Attributes.lean	feat: realizeConst for match equations (#7247)	2025-03-03 17:18:29 +00:00
AuxRecursor.lean
BuiltinDocAttr.lean
Class.lean
Compiler.lean
CoreM.lean	perf: avoid contended access to IO.Ref in isTracingEnabledFor (#7601)	2025-03-21 12:07:25 +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
Environment.lean	chore: remove the old Lean.Data.HashMap implementation (#7519)	2025-03-20 23:49:55 +00:00
Exception.lean	fix: convert kernel interrupt into elab interrupt (#6988)	2025-02-07 15:55:32 +00:00
Expr.lean	feat: Nat div/mod in cutsat (#7502)	2025-03-16 00:29:43 +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: remove >6 month old deprecations (#7518)	2025-03-17 04:42:05 +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	feat: realizeConst for match equations (#7247)	2025-03-03 17:18:29 +00:00
MonadEnv.lean	perf: remove most remaining async blockers in Init.Data.List.Sublist (#7500)	2025-03-15 15:26:06 +00:00
Namespace.lean	chore: rename HashMap.empty to HashMap.emptyWithCapacity (#7447)	2025-03-12 23:01:18 +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	feat: do not propagate pretty printer errors through messages (#3696)	2024-12-11 04:10:09 +00:00
PrivateName.lean	feat: Environment.addConstAsync (#6691)	2025-01-19 02:00:16 +00:00
ProjFns.lean
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: remove more async blockers (#7497)	2025-03-15 11:07:04 +00: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	feat: structure autoParam inheritance (#7640)	2025-03-23 06:04:00 +00:00
SubExpr.lean
Syntax.lean	feat: cleanup of get and back functions on List/Array (#7059)	2025-02-17 01:43:45 +00:00
ToExpr.lean	feat: ToExpr IntX (#7268)	2025-02-28 09:32:30 +00:00
ToLevel.lean	feat: upstream ToLevel from mathlib (#6285)	2024-12-05 05:50:32 +00:00
Util.lean	feat: simp +arith sorts linear atoms (#7040)	2025-02-11 23:37:30 +00:00
Widget.lean