max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src
History
Kyle Miller a310488b7f
chore: refactor structure command, fixes (#5842) 
Refactors the `structure` command to support recursive structures. These
are disabled for now, pending additional elaborator support in #5822.
This refactor is also a step toward `structure` appearing in `mutual`
blocks.

Error reporting is now more precise, and this fixes an issue where
general errors could appear on the last field. Adds "don't know how to
synthesize placeholder" errors for default values.

Closes #2512
2024-10-25 19:46:17 +00:00
..
bin
cmake feat: compile against Windows SDK headers under Windows (#5753) 2024-10-22 13:00:02 +00:00
include/lean feat: define Int8 (#5790) 2024-10-25 06:06:40 +00:00
Init feat: Array.forIn', and relate to List (#5833) 2024-10-25 07:24:39 +00:00
initialize fix: explicitly initialize Std in lean_initialize (#4668) 2024-07-06 13:17:30 +00:00
kernel fix: instantiateMVars slowdown in the language server (#5805) 2024-10-25 09:35:41 +00:00
lake feat: rename Array.shrink to take, and relate to List.take (#5796) 2024-10-21 23:35:32 +00:00
Lean chore: refactor structure command, fixes (#5842) 2024-10-25 19:46:17 +00:00
library chore: remove repeated words (#5438) 2024-09-24 03:40:11 +00:00
runtime feat: define Int8 (#5790) 2024-10-25 06:06:40 +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 feat: define Int8 (#5790) 2024-10-25 06:06:40 +00:00
cadical.mk feat: ship cadical (#4325) 2024-08-23 09:13:27 +00:00
CMakeLists.txt feat: define Int8 (#5790) 2024-10-25 06:06:40 +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 feat: System.Platform.target (#3207) 2024-01-24 12:11:00 +00:00