max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta
History
Joachim Breitner 032c0257c3 feat: DiscrTree: index the domain of ∀ 
It bothered me that inferring instances of the shape `Decidable (∀ (x : Fin _), _)`
will go linearly through all instances of that shape, even those that are
about `∀ (x : Nat), …`. And that  `Decidable (∃ (x : Fin _), _)` gets better
indexing than `Decidable (∀ (x : Fin _), _)`.

Judging from code comments, the discr tree used to index arrow types
with two arguments (domain and body), and that led to bugs due to the
dependency, so the arguments were removed. But it seems that indexing
the domain is completely simple and innocent.

So let’s see what happens…

Mostly only insignificant perf improvements, unfortunately (~Mathlib.Data.Matroid.IndepAxioms — instructions -11.4B, overall build instructions -0.097 %):
http://speed.lean-fro.org/mathlib4/compare/dd333cc1-fa26-42f2-96c6-b0e66047d0b6/to/6875ff8f-a17c-431d-8b8b-2f00799be794

This is just a small baby step compared to the more invasive improvements
done in the [`RefinedDiscrTree` by  J. W. Gerbscheid](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/FunProp/RefinedDiscrTree.html) in mathlib.
2024-10-16 13:35:31 +02:00
..
ArgsPacker chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Constructions chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Match chore: remove repeated words (#5438) 2024-09-24 03:40:11 +00:00
Tactic fix: ac_nf0, simp_arith: don't tempt the kernel to reduce atoms (#5708) 2024-10-16 08:52:58 +00:00
AbstractMVars.lean chore: switch to Std.HashMap and Std.HashSet almost everywhere 2024-08-07 18:24:42 +02:00
AbstractNestedProofs.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ACLt.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
AppBuilder.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
ArgsPacker.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
Basic.lean feat: better #eval command (#5627) 2024-10-08 20:51:46 +00:00
Canonicalizer.lean chore: deprecate Lean.HashMap and Lean.HashSet (#4954) 2024-08-08 12:46:10 +00:00
Check.lean feat: export Bool.and/or/not/xor 2024-09-16 12:45:51 +10:00
CheckTactic.lean chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508) 2024-03-04 23:56:30 +00:00
Closure.lean chore: switch to Std.HashMap and Std.HashSet almost everywhere 2024-08-07 18:24:42 +02:00
Coe.lean refactor: Offset.lean and related files (#3614) 2024-03-05 19:40:15 -08:00
CoeAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
CollectFVars.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08: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 refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
Constructions.lean refactor: Split Constructions module (#4656) 2024-07-05 08:25:44 +00:00
CtorRecognizer.lean feat: allow users to disable simpCtorEq simproc (#5167) 2024-08-26 13:51:21 +00:00
DecLevel.lean chore: missing registerTraceClass (#4369) 2024-06-06 00:53:16 +00:00
Diagnostics.lean chore: wrap diagnostic results in MessageData.traces (#4897) 2024-08-06 19:10:51 +00:00
DiscrTree.lean feat: DiscrTree: index the domain of ∀ 2024-10-16 13:35:31 +02:00
DiscrTreeTypes.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
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: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
ExprLens.lean chore: code convention (#4009) 2024-04-28 15:49:55 +00:00
ExprTraverse.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ForEachExpr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
FunInfo.lean fix: getFunInfo, inferType to use withAtLeastTransparency, not withTransparency (#5563) 2024-10-04 13:04:35 +00:00
GeneralizeTelescope.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
GeneralizeVars.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
GetUnfoldableConst.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
GlobalInstances.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
IndPredBelow.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
Inductive.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
InferType.lean fix: getFunInfo, inferType to use withAtLeastTransparency, not withTransparency (#5563) 2024-10-04 13:04:35 +00:00
Injective.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Instances.lean fix: upgrade instance synth order issues to hard errors (#5399) 2024-10-08 23:29:59 +00:00
Iterator.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
KAbstract.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
KExprMap.lean chore: switch to Std.HashMap and Std.HashSet almost everywhere 2024-08-07 18:24:42 +02:00
LazyDiscrTree.lean chore: update copyrights (#5449) 2024-09-24 05:27:53 +00:00
LevelDefEq.lean feat: universe constraint approximations (#3981) 2024-04-24 20:27:51 +00:00
LitValues.lean feat: simprocs for #[1,2,3,4,5][2] (#4765) 2024-07-17 03:05:17 +00:00
Match.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MatchUtil.lean fix: regression on match expressions with builtin literals (#3521) 2024-02-27 18:49:44 +00:00
NatInstTesters.lean feat: shorten auto-generated instance names (#3089) 2024-04-13 18:08:50 +00:00
Offset.lean chore: remove (syntactically) duplicate imports (#5437) 2024-09-23 23:07:56 +00:00
PPGoal.lean fix: have Lean.Meta.ppGoal use hard newlines (#5640) 2024-10-08 17:36:08 +00:00
PProdN.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
RecursorInfo.lean refactor: remove mkRecursorInfoForKernelRec (#5681) 2024-10-15 15:59:04 +00:00
Reduce.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
ReduceEval.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SizeOf.lean refactor: more idiomatic syntax for if h: (#5567) 2024-10-01 15:23:54 +00:00
Structure.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
SynthInstance.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00
Tactic.lean feat: add grind_norm simp attribute for grind tactic 2024-05-14 19:52:25 +02:00
Transform.lean feat: decide! tactic for using kernel reduction (#5665) 2024-10-11 06:40:57 +00:00
TransparencyMode.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
UnificationHint.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
WHNF.lean chore: fix spelling mistakes in src/Lean/Meta/ (#5436) 2024-09-23 23:09:14 +00:00