Mac Malone 77609dcdc7 feat: lake: config field autocomplete in whitespace (#7393) ... This PR adds autocompletion support for Lake configuration fields in the Lean DSL at the indented whitespace after an existing field. Autocompletion in the absence of any fields is currently still not supported. **Breaking change:** The nonstandard braced configuration syntax now uses a semicolon `;` rather than a comma `,` as a separator. Indentation can still be used as an alternative to the separator.		2025-03-10 15:37:39 +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	feat: lemmas about pure for {List,Array,Vector}.{mapM,foldlM,foldrM,anyM,allM,findM?,findSomeM?} (#7356)	2025-03-10 13:55:17 +00:00
initialize
kernel	fix: bv_omega to use -implicitDefEqProofs (#7387)	2025-03-09 00:13:14 +00:00
lake	feat: lake: config field autocomplete in whitespace (#7393)	2025-03-10 15:37:39 +00:00
Lean	feat: bv_decide support enum inductive matches with default branches (#7417)	2025-03-10 14:05:04 +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
Std	feat: tree map lemmas for modify (#7419)	2025-03-10 14:35:24 +00:00
util	fix: set CP_UTF8 on Windows (#7213)	2025-02-26 18:36:32 +00:00
cadical.mk
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