From a79b50d62902cf7b51eaefa2b07ecd52b3babf12 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 31 Aug 2021 10:06:22 -0700 Subject: [PATCH] chore: add type to error message --- src/Lean/Elab/Extra.lean | 2 +- tests/lean/calcErrors.lean.expected.out | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index f694b5c9d1..d30ccc39d3 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -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 diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out index 0dfff31784..88c20db28a 100644 --- a/tests/lean/calcErrors.lean.expected.out +++ b/tests/lean/calcErrors.lean.expected.out @@ -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