max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add type to error message

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-31 10:06:22 -07:00
parent c391521891
commit a79b50d629
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Extra.lean
View file

@ -258,7 +258,7 @@ def elabBinCalc : TermElab := fun stx expectedType? => do
for stepStx in stepStxs do
let type ← elabType stepStx[0]
let some (_, lhs, _) ← relation? type |
throwErrorAt stepStx[0] "invalid 'calc' step, relation expected"
throwErrorAt stepStx[0] "invalid 'calc' step, relation expected{indentExpr type}"
if types.size > 0 then
let some (_, _, prevRhs) ← relation? types.back | unreachable!
unless (← isDefEqGuarded lhs prevRhs) do

1
tests/lean/calcErrors.lean.expected.out
View file

@ -9,6 +9,7 @@ calcErrors.lean:7:8-7:29: error: invalid 'calc' step, left-hand-side is
previous right-hand-side is
b + b : Nat
calcErrors.lean:15:8-15:11: error: invalid 'calc' step, relation expected
p a
calcErrors.lean:20:8-20:19: error: invalid 'calc' step, failed to synthesize `Trans` instance
Trans p p ?m
calcErrors.lean:27:7-27:12: error: invalid 'calc' step, left-hand-side is