Leonardo de Moura 945abe0065 fix: unused let_fun elimination in simp (#6375) ... This PR fixes a bug in the simplifier. It was producing terms with loose bound variables when eliminating unused `let_fun` expressions. This issue was affecting the example at #6374. The example is now timing out.		2024-12-13 01:18:46 +00:00
..
BuiltinSimprocs	chore: remove deprecated aliases for Int.tdiv and Int.tmod (#6322)	2024-12-08 05:19:42 +00:00
Attr.lean	refactor: mark the Simp.Context constructor as private	2024-11-13 14:12:55 +11:00
BuiltinSimprocs.lean	feat: simprocs for #[1,2,3,4,5][2] (#4765)	2024-07-17 03:05:17 +00:00
Diagnostics.lean	feat: make it possible to use dot notation in m! strings (#5857)	2024-10-27 22:55:29 +00:00
Main.lean	fix: unused let_fun elimination in simp (#6375)	2024-12-13 01:18:46 +00:00
RegisterCommand.lean	feat: attribute [simp ←] (#5870)	2024-10-29 11:07:08 +00:00
Rewrite.lean	feat: Simp.Config.implicitDefEqProofs (#4595)	2024-11-29 22:29:27 +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	fix: isDefEq, whnf, simp caching and configuration (#6053)	2024-11-18 01:17:26 +00:00
Types.lean	fix: isDefEq, whnf, simp caching and configuration (#6053)	2024-11-18 01:17:26 +00:00