Kim Morrison 781e3c6add chore: remove unhelpful grind annotations (#10435) ... This PR removes some `grind` annotations for `Array.attach` and related functions. These lemmas introduce lambda on the right hand side which `grind` can't do much with. I've added a test file that verifies that the theorems with removed annotations can actually be proved already by grind. Removing the annotations will help with excessive instantiation.		2025-09-24 03:02:46 +00:00
..
Control	chore: missing grind modifiers and local grind theorems config (#10428)	2025-09-17 16:15:16 +00:00
Data	chore: remove unhelpful grind annotations (#10435)	2025-09-24 03:02:46 +00:00
Grind	feat: helper ordered ring theorems (#10529)	2025-09-24 03:01:19 +00:00
GrindInstances	chore: move String.utf8EncodeChar to the prelude (#10264)	2025-09-07 12:42:53 +00:00
Internal	feat: add more MonoBind instances for monad transformers (#10230)	2025-09-03 17:15:41 +00:00
Meta	refactor: split Init.Meta in preparation for meta semantics restrictions (#10343)	2025-09-11 13:01:03 +00:00
Omega	chore: reorganize Init imports around strings (#10289)	2025-09-07 17:09:14 +00:00
System	chore: remove >6 month old deprecations (#10446)	2025-09-22 12:47:11 +00:00
BinderNameHint.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
BinderPredicates.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
ByCases.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Classical.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Coe.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Control.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Conv.lean	feat: add enter [in patt] syntax (#10081)	2025-08-23 17:16:53 +00:00
Core.lean	feat: redefine String, part one (#10304)	2025-09-18 11:36:52 +00:00
Data.lean	feat: dyadic rationals (#9993)	2025-08-26 03:49:39 +00:00
Dynamic.lean	perf: do not export opaque bodies (#10119)	2025-08-27 20:59:59 +00:00
Ext.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
GetElem.lean	chore: remove >6 month old deprecations (#10446)	2025-09-22 12:47:11 +00:00
Grind.lean	feat: helper definitions for injective function support in grind (#10445)	2025-09-18 19:42:15 +00:00
GrindInstances.lean	feat: upstream several Rat lemmas from mathlib (#10077)	2025-08-25 06:02:27 +00:00
Guard.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Hints.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Internal.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
LawfulBEqTactics.lean	feat: linear-size BEq instance (#10268)	2025-09-18 21:27:25 +00:00
MacroTrace.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Meta.lean	refactor: split Init.Meta in preparation for meta semantics restrictions (#10343)	2025-09-11 13:01:03 +00:00
MetaTypes.lean	doc: improve docstrings for simp!, simp_all!, dsimp! and autoUnfold (#9991)	2025-09-09 13:34:16 +00:00
MethodSpecsSimp.lean	feat: @[method_specs_simp] in Init (#10407)	2025-09-16 10:27:33 +00:00
Notation.lean	chore: remove bootstrapping workaround (#10484)	2025-09-21 07:36:49 +00:00
NotationExtra.lean	feat: overhaul meta system (#10362)	2025-09-17 21:04:29 +00:00
Omega.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Prelude.lean	feat: redefine String, part one (#10304)	2025-09-18 11:36:52 +00:00
PropLemmas.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
RCases.lean	fix: add missing spaces for pretty printing (#9475)	2025-07-23 19:35:04 +00:00
ShareCommon.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
SimpLemmas.lean	fix: performance issue when elaborating match-expressions with many literals (#9372)	2025-07-15 03:52:23 +00:00
Simproc.lean	feat: overhaul meta system (#10362)	2025-09-17 21:04:29 +00:00
SizeOf.lean	feat: redefine String, part one (#10304)	2025-09-18 11:36:52 +00:00
SizeOfLemmas.lean	chore: avoid confusing public import all combination (#10051)	2025-08-22 12:04:42 +00:00
Syntax.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
System.lean	chore: remove >6 month old deprecations (#9640)	2025-08-05 02:29:15 +00:00
Tactics.lean	doc: fix comment about String.fromUTF8 replacing invalid chars (#10240)	2025-09-23 10:19:20 +00:00
TacticsExtra.lean	feat: overhaul meta system (#10362)	2025-09-17 21:04:29 +00:00
Task.lean	refactor: implement IO.waitAny using Lean (#9732)	2025-08-06 13:09:15 +00:00
Try.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
Util.lean	chore: reorganize Init imports around strings (#10289)	2025-09-07 17:09:14 +00:00
WF.lean	feat: add @[grind =] to Prod.lex_def (#9609)	2025-07-29 02:45:02 +00:00
WFTactics.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00
While.lean	feat: make private the default in module (#9044)	2025-06-28 16:30:53 +00:00