de5e039c83
Summary: - Take `synthPendingDepth` into account when caching TC results - Add `maxSynthPendingDepth` option with default := 2. - Add support for tracking `synthPending` failures when using `set_option diagnostics true` closes #2522 closes #3313 closes #3927 Identical to #4114 but with `maxSynthPendingDepth := 1` closes #4114 cc @semorrison
20 lines
731 B
Text
20 lines
731 B
Text
calcErrors.lean:7:30-7:33: error: type mismatch
|
||
rfl
|
||
has type
|
||
b + b = b + b : Prop
|
||
but is expected to have type
|
||
b + b = 0 + c + b : Prop
|
||
calcErrors.lean:13:8-13:29: error: invalid 'calc' step, left-hand-side is
|
||
0 + c + b : Nat
|
||
previous right-hand-side is
|
||
b + b : Nat
|
||
calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
|
||
p a
|
||
calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
|
||
Trans p p ?m
|
||
use `set_option diagnostics true` to get diagnostic information
|
||
calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand-side is
|
||
γ : Sort u_1
|
||
previous right-hand-side is
|
||
b : β
|
||
calcErrors.lean:61:18-61:19: error: unexpected token '['; expected command
|