Arthur Adjedj 7150a0d538 fix: reduce let-bodies correctly in StructInst (#3152) ... Closes #3146 Reduction doesn't trigger correctly on the bodies of `let`-expressions in `StructInst`, leading some meta-variables to linger in the terms of some fields. Because of this, default fields may try multiple times (and fail) to be generated, leading to an unexpected error. The solution implemented here is to modify the values of the introduced variables in the local context so as to reduce them correctly.		2024-10-24 23:33:33 +00:00
..
bin
cmake	feat: compile against Windows SDK headers under Windows (#5753)	2024-10-22 13:00:02 +00:00
include/lean	feat: use libuv for tempfiles (#5135)	2024-10-14 13:56:56 +00:00
Init	chore: cleanup imports (#5825)	2024-10-23 23:51:13 +00:00
initialize	fix: explicitly initialize Std in lean_initialize (#4668)	2024-07-06 13:17:30 +00:00
kernel	perf: has_univ_mvar, has_univ_mvar, and has_fvar in C++ (#5793)	2024-10-21 16:56:30 +00:00
lake	feat: rename Array.shrink to take, and relate to List.take (#5796)	2024-10-21 23:35:32 +00:00
Lean	fix: reduce let-bodies correctly in StructInst (#3152)	2024-10-24 23:33:33 +00:00
library	chore: remove repeated words (#5438)	2024-09-24 03:40:11 +00:00
runtime	feat: use libuv for tempfiles (#5135)	2024-10-14 13:56:56 +00:00
shell	chore: avoid rebuilding leanmanifest in each build (#5057)	2024-08-15 14:55:36 +00:00
Std	feat: bv_decide BitVec.sdiv (#5823)	2024-10-23 21:10:27 +00:00
util	fix: help message flags, removes -f flag and adds -g flag (#5685)	2024-10-13 06:37:09 +00:00
cadical.mk	feat: ship cadical (#4325)	2024-08-23 09:13:27 +00:00
CMakeLists.txt	feat: compile against Windows SDK headers under Windows (#5753)	2024-10-22 13:00:02 +00:00
config.h.in
githash.h.in
Init.lean	chore: make 'while' available earlier (#5784)	2024-10-21 05:56:37 +00:00
lakefile.toml.in	feat: introduce Std (#4499)	2024-06-21 07:08:45 +00:00
lean-toolchain
Lean.lean	chore: remove SplitIf.ext cache (#5571)	2024-10-17 09:36:00 +00:00
lean.mk.in	fix: split libleanshared on Windows to avoid symbol limit	2024-08-12 14:14:42 +02:00
Leanc.lean	feat: expose flags for the bundled C compiler (#4477)	2024-06-22 01:23:33 +00:00
Std.lean	chore: move Lean.Data.Parsec to Std.Internal.Parsec (#5115)	2024-08-21 15:26:17 +00:00
stdlib.make.in	fix: rm new shared libs before build for Windows (#5541)	2024-10-02 04:06:03 +00:00
stdlib_flags.h	chore: unset parseQuotWithCurrentStage in stage1’s src/stdlib_flags.h (#4537)	2024-06-23 09:44:14 +00:00
version.h.in