max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
jrr6 fa1da03d50
feat: update structure/inductive error messages (#9592) 
This PR updates the styling and wording of error messages produced in
inductive type declarations and anonymous constructor notation,
including hints for inferable constructor visibility updates.
2025-07-29 21:27:30 +00:00
..
Compiler perf: during specialization, don't abstract all local fun decls under binders (#9596) 2025-07-28 17:36:43 +00:00
Data feat: improve set_option error messages (#9496) 2025-07-26 02:04:45 +00:00
DocString refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Elab feat: update structure/inductive error messages (#9592) 2025-07-29 21:27:30 +00:00
ErrorExplanations refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Language refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Linter refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00
Meta feat: Add List.zipWithM and Array.zipWithM (#9528) 2025-07-28 08:39:52 +00:00
Parser refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00
ParserCompiler refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
PrettyPrinter perf: optimize Name.toString (#9594) 2025-07-29 07:20:56 +00:00
Server refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00
Util refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Widget refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00
AddDecl.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Attributes.lean refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00
AuxRecursor.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
BuiltinDocAttr.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Class.lean refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00
Compiler.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
CoreM.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Data.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Declaration.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
DeclarationRange.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
DefEqAttrib.lean refactor: minimize Lean.DefEqAttrib imports (#9543) 2025-07-25 15:18:17 +00:00
DocString.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Elab.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
EnvExtension.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Environment.lean chore: remove syntax for extern arity specifications (#9556) 2025-07-26 00:44:36 +00:00
ErrorExplanation.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ErrorExplanations.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Exception.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Expr.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
HeadIndex.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Hygiene.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ImportingFlag.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
InternalExceptionId.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
KeyedDeclsAttribute.lean refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00
LabelAttribute.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Level.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Linter.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
LoadDynlib.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
LocalContext.lean doc: clarify nondep behaviour (#9570) 2025-07-26 22:46:48 +00:00
Log.lean fix: widgets broken by overzealous modularization (#9548) 2025-07-25 16:51:18 +00:00
Message.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Meta.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
MetavarContext.lean doc: clarify nondep behaviour (#9570) 2025-07-26 22:46:48 +00:00
Modifiers.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
MonadEnv.lean perf: remove grind blockers (#9328) 2025-07-26 06:15:33 +00:00
Namespace.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Parser.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ParserCompiler.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
PremiseSelection.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
PrettyPrinter.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
PrivateName.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ProjFns.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ReducibilityAttrs.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Replay.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ReservedNameAction.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ResolveName.lean fix: avoid RPC errors in nonexistent identifier hovers (#9494) 2025-07-26 02:04:43 +00:00
Runtime.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ScopedEnvExtension.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Server.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Setup.lean perf: do not even open .olean.server when not necessary (#9531) 2025-07-25 14:52:24 +00:00
Shell.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Structure.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
SubExpr.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Syntax.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ToExpr.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ToLevel.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Util.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Widget.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00