max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Grind
History
Kim Morrison 0ab69a32cb
chore: parameterize NoNatZeroDivisors by NatModule instead of HMul (#9527) 
This PR changes `Lean.Grind.NoNatZeroDivisors` so that it is
parametrised by a `NatModule` instance rather than just a `HMul`
instance. This is sufficiently general for our purposes, and is a
band-aid (~40% improvement) for the performance problems we've been
seeing coming from inference here. The problems observed in Mathlib may
not see much improvement, however.
2025-07-25 08:46:05 +00:00
..
Module chore: parameterize NoNatZeroDivisors by NatModule instead of HMul (#9527) 2025-07-25 08:46:05 +00:00
Ordered fix: refactor grind's module/ring design to avoid a diamond (#9168) 2025-07-03 06:50:46 +00:00
Ring fix: definition of Lean.Grind.Field (#9520) 2025-07-25 00:35:43 +00:00
Attr.lean feat: pattern inference using symbol priorities in grind (#9182) 2025-07-03 16:47:38 -07:00
Cases.lean feat: attribute [grind cases eager] PProd MProd (#9121) 2025-07-01 04:02:47 +00:00
Ext.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Lemmas.lean perf: propagateEqUp (#9326) 2025-07-12 03:09:59 +00:00
Module.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Norm.lean refactor: support for Nat in grind cutsat (#9340) 2025-07-13 23:40:03 +00:00
Offset.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Ordered.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
PP.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Propagator.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Ring.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Tactics.lean fix: improve evalInt? (#9479) 2025-07-23 01:51:04 +00:00
ToInt.lean perf: synthesize ToInt instances on demand (#9241) 2025-07-08 02:36:16 +00:00
ToIntLemmas.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Util.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00