Joachim Breitner c797525d2a fix: WellFounded preprocessing: use dsimp (#7409) ... This PR allows the use of `dsimp` during preprocessing of well-founded definitions. This fixes regressions when using `if-then-else` without giving a name to the condition, but where the condition is needed for the termination proof, in cases where that subexpression is reachable only by dsimp, but not by simp (e.g. inside a dependent let) Also fixes some preprocessing lemmas to not be bad simp lemmas (with lambdas on the LHS, due to dot notation and unfortunate argument order) This fixes #7408.		2025-03-09 22:19:16 +00:00
..
bin	feat: API to avoid deadlocks from dropped promises (#6958)	2025-02-07 15:33:10 +00:00
cmake	fix: Windows stage0 linking (#6622)	2025-01-14 09:09:50 +01:00
include/lean	feat: IntX.abs (#7131)	2025-02-18 13:16:30 +00:00
Init	fix: WellFounded preprocessing: use dsimp (#7409)	2025-03-09 22:19:16 +00:00
initialize	fix: explicitly initialize Std in lean_initialize (#4668)	2024-07-06 13:17:30 +00:00
kernel	fix: bv_omega to use -implicitDefEqProofs (#7387)	2025-03-09 00:13:14 +00:00
lake	chore: lake: revert builtin inits, elabs, & macros (#7399)	2025-03-09 01:52:50 +00:00
Lean	fix: WellFounded preprocessing: use dsimp (#7409)	2025-03-09 22:19:16 +00:00
library	fix: properly handle scoping of join point candidates in cce (#7398)	2025-03-08 18:10:41 +00:00
runtime	perf: use free_sized in mpz.cpp (#6825)	2025-03-03 08:47:15 +00:00
shell	chore: avoid rebuilding leanmanifest in each build (#5057)	2024-08-15 14:55:36 +00:00
Std	feat: add more multiplication lemmas to bv_normalize (#7407)	2025-03-09 18:14:30 +00:00
util	fix: set CP_UTF8 on Windows (#7213)	2025-02-26 18:36:32 +00:00
cadical.mk	feat: ship cadical (#4325)	2024-08-23 09:13:27 +00:00
CMakeLists.txt	chore: begin development cycle for v4.19.0 (#7299)	2025-03-03 11:01:21 +00:00
config.h.in
githash.h.in
Init.lean	feat: binderNameHint (#6947)	2025-02-06 11:03:27 +00:00
lakefile.toml.in	feat: Lake plugin w/ USE_LAKE (#7233)	2025-02-26 04:05:15 +00:00
lean-toolchain
Lean.lean	feat: use realizeConst for all equation, unfold, induction, and partial fixpoint theorems (#7261)	2025-03-06 15:38:04 +00:00
lean.mk.in	feat: use realizeConst for all equation and unfold theorems (#7348)	2025-03-05 14:56:50 +00:00
Leanc.lean
Std.lean	feat: Std.Net.Addr (#6563)	2025-01-09 09:33:03 +00:00
stdlib.make.in	fix: make the stage2 Leanc build use stage2 oleans rather than stage1 oleans (#7190)	2025-02-25 06:20:50 +00:00
stdlib_flags.h	feat: add debug.proofAsSorry (#6300)	2024-12-03 23:21:38 +00:00
version.h.in	chore: tag prerelease builds with -pre (#5943)	2024-11-06 14:47:52 +00:00