jrr6 0002ea8a37 feat: pre-stage0 groundwork for named error messages (#8649) ... This PR adds the pre-stage0-update infrastructure for named error messages. It adds macro syntax for registering and throwing named errors (without elaborators), mechanisms for displaying error names in the Infoview and at the command line, and the ability to link to error explanations in the manual (once they are added).		2025-06-11 14:52:08 +00:00
..
Tactic	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
Term	feat: recommended_spelling command (#6869)	2025-02-03 11:15:52 +00:00
Attr.lean	feat: more infrastructure for tactic documentation (#4490)	2024-06-21 12:49:30 +00:00
Basic.lean	feat: := private instance syntax	2025-05-28 10:18:04 +02:00
Command.lean	feat: pre-stage0 groundwork for named error messages (#8649)	2025-06-11 14:52:08 +00:00
Do.lean	fix: allow ascii <- in if let clauses (#8102)	2025-04-27 13:17:58 +00:00
Extension.lean	feat: quotations for parser aliases (#4307)	2024-05-30 09:22:22 +00:00
Extra.lean	chore: remove old documentation site (#7974)	2025-05-14 14:31:33 +00:00
Level.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Module.lean	feat: meta syntax	2025-06-04 18:26:05 +02:00
StrInterpolation.lean	feat: @[builtin_doc] attribute (part 2) (#3918)	2024-09-13 08:05:10 +00:00
Syntax.lean	perf: add prelude to all Lean modules	2024-02-18 14:55:17 -08:00
Tactic.lean	feat: decide +revert and improvements to native_decide (#5999)	2024-11-08 18:17:46 +00:00
Term.lean	feat: pre-stage0 groundwork for named error messages (#8649)	2025-06-11 14:52:08 +00:00
Types.lean	feat: cleanup of get and back functions on List/Array (#7059)	2025-02-17 01:43:45 +00:00