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

chore: calc: improve error range

Browse source
This commit is contained in:
Gabriel Ebner 2023-02-02 14:21:06 -08:00
parent 35ccf7b163
commit 8265d8bb13
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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. -/

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

@ -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