jrr6 fb462fdf9e feat: add named argument hints (#9315) ... This PR adds improves the "invalid named argument" error message in function applications and match patterns by providing clickable hints with valid argument names. In so doing, it also fixes an issue where this error message would erroneously flag valid match-pattern argument names.		2025-07-17 03:22:25 +00:00
..
Compiler	refactor: remove special cases for subsingleton casesOn (#9412)	2025-07-16 23:41:41 +00:00
Data	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
DocString	perf: do not import non-meta IR	2025-06-27 08:13:31 -07:00
Elab	feat: add named argument hints (#9315)	2025-07-17 03:22:25 +00:00
ErrorExplanations	fix: error explanation needs updating (#9091)	2025-06-30 05:10:04 +00:00
Language	chore: allow use of the module system in all of core (#9078)	2025-06-29 13:49:27 +00:00
Linter	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
Meta	feat: add named argument hints (#9315)	2025-07-17 03:22:25 +00:00
Parser	fix: order of @[expose] public section	2025-07-16 13:32:11 +02:00
ParserCompiler
PrettyPrinter	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
Server	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
Util	fix: adjust unsafe trick for upcoming optimization (#9393)	2025-07-16 00:10:01 +00:00
Widget	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
AddDecl.lean	fix: module system: remove WellFounded-specific hacks (#9143)	2025-07-02 11:58:50 +00:00
Attributes.lean	feat: explicit defeq attribute (#8419)	2025-06-06 18:40:06 +00:00
AuxRecursor.lean	refactor: remove binductionOn, use brecOn instead (#8820)	2025-06-17 07:07:24 +00:00
BuiltinDocAttr.lean	chore: follow up on #8173 post-stage0 update (#8722)	2025-06-16 09:08:35 +00:00
Class.lean	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
Compiler.lean	chore: remove now-unused Lean.Compiler.AtMostOnce (#9278)	2025-07-09 14:31:15 +00:00
CoreM.lean	refactor: Expose DeclNameGenerator idx (#9020)	2025-07-13 10:24:04 +00:00
Data.lean
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
Elab.lean	feat: add elaborators, completions, and hovers for named errors (#8730)	2025-06-18 15:51:34 +00:00
EnvExtension.lean	refactor: environment extension state splitting (#8653)	2025-06-11 12:52:04 +00:00
Environment.lean	fix: assorted module system fixes (#9406)	2025-07-16 13:31:08 +00:00
ErrorExplanation.lean	feat: add elaborators, completions, and hovers for named errors (#8730)	2025-06-18 15:51:34 +00:00
ErrorExplanations.lean	feat: improve projection and field-notation errors (#8986)	2025-06-26 18:36:47 +00:00
Exception.lean	feat: add initial error explanations (#8934)	2025-06-23 17:24:09 +00:00
Expr.lean	refactor: support for Nat in grind cutsat (#9340)	2025-07-13 23:40:03 +00:00
HeadIndex.lean
Hygiene.lean
ImportingFlag.lean
InternalExceptionId.lean
KeyedDeclsAttribute.lean
LabelAttribute.lean
Level.lean
Linter.lean	feat: linter.unusedSimpArgs (#8901)	2025-06-22 09:10:21 +00:00
LoadDynlib.lean
LocalContext.lean	feat: add usedLetOnly to LocalContext binder functions (#9131)	2025-07-01 18:41:49 +00:00
Log.lean	chore: enable error explanation widget (#9043)	2025-06-27 19:25:29 +00:00
Message.lean	refactor: replace some Subarray functions with generic slice functions (#9017)	2025-07-03 19:33:19 +00:00
Meta.lean	feat: add Meta.letToHave and the let_to_have tactic (#8954)	2025-06-24 01:33:53 +00:00
MetavarContext.lean	refactor: migrate all usages of old slice notation (#9000)	2025-06-27 18:52:07 +00:00
Modifiers.lean	fix: assorted module system fixes (#9406)	2025-07-16 13:31:08 +00:00
MonadEnv.lean	feat: meta phase restrictions	2025-06-12 16:36:08 +02:00
Namespace.lean
Parser.lean
ParserCompiler.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
PremiseSelection.lean
PrettyPrinter.lean	feat: prettier expected type mismatch error message (#9099)	2025-07-01 07:50:53 +00:00
PrivateName.lean
ProjFns.lean
ReducibilityAttrs.lean	chore: use note and hint' for message addenda (#8980)	2025-06-27 15:16:01 +00:00
Replay.lean
ReservedNameAction.lean	feat: make equational theorems of non-exposed defs private (#8519)	2025-06-04 11:52:08 +00:00
ResolveName.lean	feat: allow access to private names through import all (#8828)	2025-06-27 12:13:46 +00:00
Runtime.lean
ScopedEnvExtension.lean	fix: do not export private instances (#9407)	2025-07-16 18:59:48 +00:00
Server.lean
Setup.lean	perf: do not import non-meta IR	2025-06-27 08:13:31 -07:00
Shell.lean	feat: ignore lean -R if module name is in setup (#8874)	2025-06-23 17:55:52 +00:00
Structure.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
SubExpr.lean
Syntax.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
ToExpr.lean
ToLevel.lean
Util.lean	feat: server support for new module setup (#8699)	2025-06-23 18:00:14 +00:00
Widget.lean