diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean index 46a30a7575..8c963ad64c 100644 --- a/src/Lean/Elab/Calc.lean +++ b/src/Lean/Elab/Calc.lean @@ -92,7 +92,7 @@ def elabCalcSteps (steps : Array Syntax) : TermElabM Expr := do let mut result := proofs[0]! let mut resultType := types[0]! for i in [1:proofs.size] do - (result, resultType) ← withRef steps[i]! <| mkCalcTrans result resultType proofs[i]! types[i]! + (result, resultType) ← withRef steps[i]![0] <| mkCalcTrans result resultType proofs[i]! types[i]! return result /-- Elaborator for the `calc` term mode variant. -/ diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out index 4213daac0d..8362dc9c60 100644 --- a/tests/lean/calcErrors.lean.expected.out +++ b/tests/lean/calcErrors.lean.expected.out @@ -10,7 +10,7 @@ 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 +calcErrors.lean:20:8-20:13: 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 γ : Sort u_1