Leonardo de Moura e288e9266b fix: bad normalization rule in grind, and missing dsimproc (#7553) ... This PR removes a bad normalization rule in `grind`, and adds a missing dsimproc.		2025-03-18 18:32:25 +00:00
..
Arith	fix: simp +arith (#7515)	2025-03-17 03:11:48 +00:00
BuiltinSimprocs	fix: bad normalization rule in grind, and missing dsimproc (#7553)	2025-03-18 18:32:25 +00:00
Arith.lean	fix: simp +arith (#7515)	2025-03-17 03:11:48 +00:00
Attr.lean	perf: Environment blocker removals from async-proofs branch (#7483)	2025-03-14 13:37:01 +00:00
BuiltinSimprocs.lean	feat: IntX simprocs (#7228)	2025-03-03 13:37:57 +00:00
Diagnostics.lean	feat: simp diagnostics in grind (#6902)	2025-02-23 17:55:17 +00:00
Main.lean	fix: simp +arith (#7511)	2025-03-16 20:24:51 +00:00
RegisterCommand.lean	feat: attribute [simp ←] (#5870)	2024-10-29 11:07:08 +00:00
Rewrite.lean	fix: simp +arith (#7515)	2025-03-17 03:11:48 +00:00
SimpAll.lean	chore: avoid runtime array bounds checks (#6134)	2024-11-21 05:04:52 +00:00
SimpCongrTheorems.lean	feat: make it possible to use dot notation in m! strings (#5857)	2024-10-27 22:55:29 +00:00
Simproc.lean	fix: isDefEq, whnf, simp caching and configuration (#6053)	2024-11-18 01:17:26 +00:00
SimpTheorems.lean	perf: remove most remaining async blockers in Init.Data.List.Sublist (#7500)	2025-03-15 15:26:06 +00:00
Types.lean	chore: simp_arith has been deprecated (#7043)	2025-02-12 03:55:45 +00:00