Henrik Böving daf7a579ed perf: use less defeq in frequently applied bv_decide simp rules (#8208) ... This PR reduces the need for defeq in frequently used bv_decide rewrite by turning them into simprocs that work on structural equality instead. As the intended meaning of these rewrites is to simply work with structural equality anyways this should not change the proving power of `bv_decide`'s rewriter but just make it faster on certain very large problems.		2025-05-02 19:15:34 +00:00
..
bin	feat: API to avoid deadlocks from dropped promises (#6958)	2025-02-07 15:33:10 +00:00
cmake	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
include/lean	feat: optimized division without remainder for Int and Nat (#8089)	2025-04-29 07:23:35 +00:00
Init	chore: remove grind ext lemmas for List/Array/Vector (#8207)	2025-05-02 17:41:02 +00:00
initialize
kernel	fix: reducing Nat.pow, kernel interprets constant as Nat literal (#8060)	2025-04-23 13:55:20 +00:00
lake	doc: lake: add needs and native library options to README (#8190)	2025-05-01 02:16:07 +00:00
Lean	perf: use less defeq in frequently applied bv_decide simp rules (#8208)	2025-05-02 19:15:34 +00:00
library	fix: make the lcnf expr cache depend on the value of root, not just… (#8156)	2025-04-29 00:37:52 +00:00
runtime	fix: include libuv outside of namespace (#8166)	2025-04-29 22:19:17 +00:00
shell	fix: lake: import-related bugs (#8026)	2025-04-19 21:02:38 +00:00
Std	perf: use less defeq in frequently applied bv_decide simp rules (#8208)	2025-05-02 19:15:34 +00:00
util	feat: allow use of experimental module system in Init (#7919)	2025-04-22 09:09:27 +00:00
cadical.mk	fix: cadical distribution on Linux (#8201)	2025-05-02 18:25:16 +00:00
CMakeLists.txt	chore: fix reldebug preset (#8051)	2025-04-23 10:05:11 +00:00
config.h.in	perf: use mimalloc by default (#7710)	2025-03-30 22:40:41 +00:00
githash.h.in
Init.lean	chore: refine module imports (#8120)	2025-04-27 20:45:31 +00:00
lakefile.toml.in	chore: lake: bootstrap Lean include directory (#7967)	2025-04-15 23:15:53 +00:00
lean-toolchain
Lean.lean	refactor: split Lean.EnvironmentExtension from Lean.Environment (#7794)	2025-04-02 16:19:12 +00:00
lean.mk.in	chore: USE_LAKE: integrate into CMake (#4466)	2025-03-15 08:58:01 +00:00
Leanc.lean
Std.lean	chore: test that there are no orphaned modules (#8082)	2025-04-24 11:55:07 +00:00
stdlib.make.in	chore: remove lakefile copy in root and tests/ (#8054)	2025-04-22 16:03:12 +00:00
stdlib_flags.h	fix: restore what simp theorems are recorded as rfl (#8114)	2025-04-26 16:09:20 +00:00
version.h.in	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00