lean4-htt/src
Kyle Miller d10d41bc07
fix: store local context for 'don't know how to synthesize implicit argument' errors (#5658)
When named arguments introduce eta arguments, the full application
contains fvars for these eta arguments, so `MVarErrorKind.implicitArg`
needs to keep a local context for its error messages. This is because
the local context of the mvar associated to the `MVarErrorKind` is not
sufficient, since when an eta argument come after an implicit argument,
the implicit argument's mvar doesn't contain the eta argument's fvar in
its local context.

Closes #5475
2024-10-09 08:40:21 +00:00
..
bin
cmake chore: more libuv search patterns for the speedcenter (#5008) 2024-08-13 10:40:09 +02:00
include/lean fix: remove non-conforming size-0 arrays (#5564) 2024-10-01 15:05:17 +00:00
Init feat: better #eval command (#5627) 2024-10-08 20:51:46 +00:00
initialize fix: explicitly initialize Std in lean_initialize (#4668) 2024-07-06 13:17:30 +00:00
kernel feat: expose Kernel.check for debugging purposes (#5412) 2024-10-01 21:28:02 +00:00
lake fix: lake: make package extraDep intransitive (#5641) 2024-10-08 23:20:05 +00:00
Lean fix: store local context for 'don't know how to synthesize implicit argument' errors (#5658) 2024-10-09 08:40:21 +00:00
library chore: remove repeated words (#5438) 2024-09-24 03:40:11 +00:00
runtime chore: fix spelling mistakes in non-Lean files (#5430) 2024-09-23 21:11:20 +00:00
shell chore: avoid rebuilding leanmanifest in each build (#5057) 2024-08-15 14:55:36 +00:00
Std feat: support umod in bv_decide (#5652) 2024-10-08 12:47:03 +00:00
util fix: typo in run_new_frontend signature (#4685) 2024-09-25 05:42:48 +00:00
cadical.mk feat: ship cadical (#4325) 2024-08-23 09:13:27 +00:00
CMakeLists.txt chore: restore Lake build 2024-09-10 15:24:23 +10:00
config.h.in
githash.h.in
Init.lean
lakefile.toml.in
lean-toolchain
Lean.lean feat: better #eval command (#5627) 2024-10-08 20:51:46 +00:00
lean.mk.in fix: split libleanshared on Windows to avoid symbol limit 2024-08-12 14:14:42 +02:00
Leanc.lean
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
version.h.in