max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta
History
Leonardo de Moura 1fcdd7ad9a
feat: add [grind cases] and [grind cases eager] attributes (#6705) 
This PR adds the attributes `[grind cases]` and `[grind cases eager]`
for controlling case splitting in `grind`. They will replace the
`[grind_cases]` and the configuration option `splitIndPred`.

After update stage0, we will push the second part of this PR.
2025-01-20 03:01:40 +00:00
..
ArgsPacker chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Constructions feat: split Lean.Kernel.Environment from Lean.Environment (#5145) 2025-01-18 18:42:57 +00:00
Match chore: require 0 < Range.step (#6391) 2024-12-15 11:33:41 +00:00
Tactic feat: add [grind cases] and [grind cases eager] attributes (#6705) 2025-01-20 03:01:40 +00:00
AbstractMVars.lean chore: switch to Std.HashMap and Std.HashSet almost everywhere 2024-08-07 18:24:42 +02:00
AbstractNestedProofs.lean
ACLt.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
AppBuilder.lean feat: avoid some redundant proof terms in grind (#6615) 2025-01-12 23:09:39 +00:00
ArgsPacker.lean refactor: ArgsPacker.unpack to return Option (#6359) 2024-12-10 15:23:13 +00:00
Basic.lean feat: improve case-split heuristic used in grind (#6609) 2025-01-12 04:21:04 +00:00
Canonicalizer.lean chore: fix canonicalizer handling over forall/lambda (#6082) 2024-11-17 07:34:45 +00:00
Check.lean chore: add missing diff-exposing in type/value mismatch errors (#6484) 2024-12-31 17:47:12 +00:00
CheckTactic.lean
Closure.lean fix: process delayed assignment metavariables correctly in Lean.Meta.Closure (#6414) 2024-12-19 20:15:49 +00:00
Coe.lean fix: make sure monad lift coercion elaborator has no side effects (#6024) 2024-11-13 16:22:31 +00:00
CoeAttr.lean
CollectFVars.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
CollectMVars.lean chore: cleanup after export Bool.and/or/not/xor 2024-09-16 12:45:51 +10:00
CompletionName.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
CongrTheorems.lean feat: reserved names for congruence theorems (#6412) 2024-12-18 06:19:29 +00:00
Constructions.lean refactor: Split Constructions module (#4656) 2024-07-05 08:25:44 +00:00
CtorRecognizer.lean fix: have Lean.Meta.isConstructorApp'? be aware of n + k Nat offsets (#6270) 2024-12-01 18:04:32 +00:00
DecLevel.lean
Diagnostics.lean fix: add workaround for MessageData limitations (#6669) 2025-01-16 16:58:20 +00:00
DiscrTree.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
DiscrTreeTypes.lean
Eqns.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Eval.lean fix: collect level parameters in evalExpr (#3090) 2024-09-27 11:55:33 +02:00
ExprDefEq.lean refactor: getUnfoldableConst*? (#5997) 2025-01-18 23:30:40 +00:00
ExprLens.lean
ExprTraverse.lean
ForEachExpr.lean chore: avoid runtime array bounds checks (#6134) 2024-11-21 05:04:52 +00:00
FunInfo.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
GeneralizeTelescope.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
GeneralizeVars.lean
GetUnfoldableConst.lean refactor: getUnfoldableConst*? (#5997) 2025-01-18 23:30:40 +00:00
GlobalInstances.lean
IndPredBelow.lean feat: refactor List/Array.mapFinIdx to unbundle the Fin argument (#6697) 2025-01-19 10:30:18 +00:00
Inductive.lean
InferType.lean fix: check must check projections (#6398) 2024-12-16 06:42:18 +00:00
Injective.lean feat: change Array.get to take a Nat and a proof (#6032) 2024-11-12 03:30:46 +00:00
Instances.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
Iterator.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
KAbstract.lean
KExprMap.lean chore: switch to Std.HashMap and Std.HashSet almost everywhere 2024-08-07 18:24:42 +02:00
LazyDiscrTree.lean doc: fix typo reference in doc of lazy discrimination tree (#6377) 2024-12-13 07:41:04 +00:00
LevelDefEq.lean chore: mark Meta.Context.config as private (#6051) 2024-11-13 13:30:06 +11:00
LitValues.lean feat: simprocs for other Fin operations (#6295) 2024-12-03 04:42:17 +00:00
Match.lean
MatchUtil.lean
NatInstTesters.lean
Offset.lean chore: cleanup imports (#5825) 2024-10-23 23:51:13 +00:00
PPGoal.lean fix: have Lean.Meta.ppGoal use hard newlines (#5640) 2024-10-08 17:36:08 +00:00
PProdN.lean chore: rename Array.back to back! (#5897) 2024-10-31 09:18:18 +00:00
RecursorInfo.lean feat: Array.insertIdx/eraseIdx take a tactic-provided proof (#6133) 2024-11-20 09:52:38 +00:00
Reduce.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
ReduceEval.lean
SizeOf.lean chore: rename Array.back to back! (#5897) 2024-10-31 09:18:18 +00:00
Sorry.lean feat: labeled and unique sorries (#5757) 2024-12-11 23:53:02 +00:00
Structure.lean
SynthInstance.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
Tactic.lean refactor: move ext environment extension to Lean.Meta.Tactic 2025-01-17 12:31:14 -08:00
Transform.lean feat: grind preprocessing and Expr internalization (#6413) 2024-12-19 00:16:48 +00:00
TransparencyMode.lean
UnificationHint.lean fix: isDefEq, whnf, simp caching and configuration (#6053) 2024-11-18 01:17:26 +00:00
WHNF.lean refactor: getUnfoldableConst*? (#5997) 2025-01-18 23:30:40 +00:00