lean4-htt/tests
Sebastian Ullrich 4d2f2d7cc5
fix: calculate error suppression per snapshot (#4657)
Generalizes #3556 to not suppressing errors in tactic steps either when
the parse error is in a later step, as otherwise changes to the end of a
proof would affect (correctness or effectiveness of) incrementality of
preceding steps.

Fixes #4623, in combination with #4643
2024-07-08 09:54:43 +00:00
..
bench chore: fix "max dynamic symbols" metric (#4669) 2024-07-08 09:09:19 +00:00
compiler chore: fix tests 2024-06-19 20:21:34 +02:00
elabissues
ir
lean fix: calculate error suppression per snapshot (#4657) 2024-07-08 09:54:43 +00:00
pkg fix: missing unboxing in interpreter when loading initialized value (#4512) 2024-06-20 10:06:24 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain