max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init
History
Leonardo de Moura dd87739fc2
feat: grind normalizers for natCast and intCast (#10313) 
This PR adds missing `grind` normalization rules for `natCast` and
`intCast` Examples:
```
open Lean.Grind
variable (R : Type) (a b : R)

section CommSemiring
variable [CommSemiring R]

example (m n : Nat) : (m + n) • a = m • a + n • a := by grind
example (m n : Nat) : (m * n) • a = m • (n • a) := by grind

end CommSemiring

section CommRing
variable [CommRing R]

example (m n : Nat) : (m + n) • a = m • a + n • a := by grind
example (m n : Nat) : (m * n) • a = m • (n • a) := by grind
example (m n : Int) : (m * n) • (a * b) = (m • a) * (n • b) := by grind

end CommRing
```
2025-09-09 01:32:09 +00:00
..
Control feat: grind annotations for basic monad transformers (#10227) 2025-09-08 23:51:55 +00:00
Data fix: bug at Poly.combine_mul_k (#10296) 2025-09-08 02:17:11 +00:00
Grind feat: grind normalizers for natCast and intCast (#10313) 2025-09-09 01:32:09 +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
Omega chore: reorganize Init imports around strings (#10289) 2025-09-07 17:09:14 +00:00
System fix: make IO.RealWorld opaque (#9631) 2025-09-08 18:12:19 +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 chore: remove bootstrap tricks from #9951 (#10203) 2025-09-01 13:30:42 +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 (#9640) 2025-08-05 02:29:15 +00:00
Grind.lean feat: AC theorems for grind (#10093) 2025-08-24 05:02:37 +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
MacroTrace.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Meta.lean chore: reorganize Init imports around strings (#10289) 2025-09-07 17:09:14 +00:00
MetaTypes.lean feat: improve grind cutsat support for Fin n when n is not a numeral (#10022) 2025-08-21 17:25:52 +00:00
Notation.lean feat: allow position reporting in #guard_msgs (#10125) 2025-08-27 06:47:34 +00:00
NotationExtra.lean chore: warn on [expose] on private definition (#9917) 2025-08-15 11:31:33 +00:00
Omega.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Prelude.lean fix: make IO.RealWorld opaque (#9631) 2025-09-08 18:12:19 +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 chore: reorganize Init imports around strings (#10289) 2025-09-07 17:09:14 +00:00
SizeOf.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +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 chore: eliminate uses of intros x y z (#9983) 2025-08-19 06:09:13 +00:00
TacticsExtra.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +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