Joachim Breitner 4b6f07060d feat: remove support for reducible well-founded recursion (#10714) ... This PR removes support for reducible well-founded recursion, a Breaking Change. Using `@[semireducible]` on a definition by well-founded recursion prints a warning that this is no longer effective. With the upcoming module system, proofs are often not available. With this change, we remove a fringe use case hat may require proofs, and that would not be supported under the module system anyways. At least for now, direct use of `WellFounded.fix` is not affected. This fixes: #5192		2025-10-10 15:48:28 +00:00
..
Compiler	chore: more module system fixes and improvements from Mathlib porting (#10655)	2025-10-08 11:30:09 +00:00
Data	refactor: discipline around arithmetic of String.Pos.Raw (#10713)	2025-10-09 07:47:45 +00:00
DocString	refactor: discipline around arithmetic of String.Pos.Raw (#10713)	2025-10-09 07:47:45 +00:00
Elab	feat: remove support for reducible well-founded recursion (#10714)	2025-10-10 15:48:28 +00:00
ErrorExplanations	feat: overhaul meta system (#10362)	2025-09-17 21:04:29 +00:00
Language	chore: module system fixes and refinements from Mathlib porting (#10643)	2025-10-02 08:28:08 +00:00
Linter	chore: more module system fixes and improvements from Mathlib porting (#10655)	2025-10-08 11:30:09 +00:00
Meta	fix: unfold more auxillary theorems in termination checking (#10733)	2025-10-10 11:09:28 +00:00
Parser	refactor: discipline around arithmetic of String.Pos.Raw (#10713)	2025-10-09 07:47:45 +00:00
ParserCompiler	fix: some ExtraModUses (#10620)	2025-10-03 15:50:40 +00:00
PremiseSelection	feat: helper functions for premise selection API (#10512)	2025-09-24 11:45:40 +00:00
PrettyPrinter	feat: hexnum parser (#10716)	2025-10-08 21:12:03 +00:00
Server	fix: Verso docstring semantic highlighting fixes (#10662)	2025-10-10 11:57:02 +00:00
Util	doc: fix url to profile.ts source (#10628)	2025-10-07 12:41:04 +00:00
Widget	test: improve language server test coverage (#10574)	2025-09-30 11:15:03 +00:00
AddDecl.lean	chore: module system fixes and refinements from Mathlib porting (#10643)	2025-10-02 08:28:08 +00:00
Attributes.lean	chore: module system fixes and refinements from Mathlib porting (#10643)	2025-10-02 08:28:08 +00:00
AuxRecursor.lean
BuiltinDocAttr.lean	feat: docstrings with Verso syntax (#10307)	2025-09-10 07:03:57 +00:00
Class.lean
Compiler.lean	chore: remove public section from end of files (#10684)	2025-10-06 13:30:48 +00:00
CoreM.lean	fix: backtracking kernel errors under Elab.async (#10438)	2025-09-18 12:33:57 +00:00
Data.lean	chore: remove public section from end of files (#10684)	2025-10-06 13:30:48 +00:00
Declaration.lean
DeclarationRange.lean	feat: default let rec and where decls to private under the module system (#9759)	2025-08-06 15:53:51 +00:00
DefEqAttrib.lean	perf: clarify and granularize access to async env ext state (#9587)	2025-08-02 17:01:08 +00:00
DocString.lean
Elab.lean	chore: remove public section from end of files (#10684)	2025-10-06 13:30:48 +00:00
EnvExtension.lean	feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies (#10575)	2025-09-28 16:00:00 +00:00
Environment.lean	feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies (#10575)	2025-09-28 16:00:00 +00:00
ErrorExplanation.lean	feat: add useful functions in Parsec, add error variant and Std.Data.ByteSlice (#9599)	2025-09-11 14:53:41 +00:00
ErrorExplanations.lean	chore: remove public section from end of files (#10684)	2025-10-06 13:30:48 +00:00
Exception.lean	feat: docstrings with Verso syntax (#10307)	2025-09-10 07:03:57 +00:00
Expr.lean	fix: make getArg!' compute the correct arg index to access (#10567)	2025-09-26 11:54:49 +00:00
ExtraModUses.lean	feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies (#10575)	2025-09-28 16:00:00 +00:00
HeadIndex.lean
Hygiene.lean	perf: make macro scope numbering less dependent on surrounding context (#10027)	2025-08-22 13:16:02 +00:00
ImportingFlag.lean	chore: miscellaneous documentation typos (#10009)	2025-08-20 21:39:03 +00:00
InternalExceptionId.lean	chore: reorganize Init imports around strings (#10289)	2025-09-07 17:09:14 +00:00
KeyedDeclsAttribute.lean	fix: some ExtraModUses (#10620)	2025-10-03 15:50:40 +00:00
LabelAttribute.lean	chore: reorganize Init imports around strings (#10289)	2025-09-07 17:09:14 +00:00
Level.lean	fix: complete overhaul of structural recursion on inductives predicates (#9995)	2025-09-01 08:17:58 +00:00
Linter.lean	chore: remove public section from end of files (#10684)	2025-10-06 13:30:48 +00:00
LoadDynlib.lean	fix: do not allow access to private primitives in public scope (#9890)	2025-08-14 15:34:54 +00:00
LocalContext.lean	feat: clean up type annotations when elaborating declaration bodies (#9674)	2025-08-18 04:43:20 +00:00
Log.lean	chore: rename String.Pos to String.Pos.Raw (#10624)	2025-10-01 07:45:24 +00:00
Message.lean
Meta.lean	feat: @[method_specs] to generate specification theorems from class instances (#10302)	2025-09-15 11:17:06 +00:00
MetavarContext.lean	fix: remove superfluous Monad instances from some spec lemmas (#10564) (#10618)	2025-09-29 15:02:43 +00:00
Modifiers.lean	fix: privacy checks and import all (#10550)	2025-09-26 13:26:10 +00:00
MonadEnv.lean	chore: module system fixes and refinements from Mathlib porting (#10643)	2025-10-02 08:28:08 +00:00
Namespace.lean
Parser.lean	feat: hexnum parser (#10716)	2025-10-08 21:12:03 +00:00
ParserCompiler.lean	chore: minor module system fixes from batteries port (#10496)	2025-09-24 08:59:23 +00:00
PremiseSelection.lean	feat: basic premise selection algorithm based on MePo (#7844)	2025-09-23 06:40:22 +00:00
PrettyPrinter.lean
PrivateName.lean
ProjFns.lean
ReducibilityAttrs.lean	chore: use ofConstName in error messages (#10121)	2025-08-25 23:20:36 +00:00
Replay.lean
ReservedNameAction.lean
ResolveName.lean	fix: privacy checks and import all (#10550)	2025-09-26 13:26:10 +00:00
Runtime.lean
ScopedEnvExtension.lean	feat: change delimiting of local attributes in implicit sections (#9968)	2025-08-28 15:48:42 +00:00
Server.lean	chore: remove public section from end of files (#10684)	2025-10-06 13:30:48 +00:00
Setup.lean	feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies (#10575)	2025-09-28 16:00:00 +00:00
Shell.lean	refactor: port more of shell.cpp to Lean (#10086)	2025-08-26 20:02:42 +00:00
Structure.lean	chore: error messages consistency (#10143)	2025-08-26 17:55:43 +00:00
SubExpr.lean
Syntax.lean	refactor: discipline around arithmetic of String.Pos.Raw (#10713)	2025-10-09 07:47:45 +00:00
ToExpr.lean	chore: kernel changes ahead of String redefinition (#10330)	2025-09-17 09:12:07 +00:00
ToLevel.lean
Util.lean	chore: remove public section from end of files (#10684)	2025-10-06 13:30:48 +00:00
Widget.lean	chore: remove public section from end of files (#10684)	2025-10-06 13:30:48 +00:00