From 75e95f93a9b2fc754fc6801d52a6dd196ac82e02 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 27 Apr 2021 11:27:46 +0200 Subject: [PATCH] feat: improve `let` error locality --- src/Lean/Elab/Binders.lean | 4 ++-- tests/lean/have.lean | 5 +++++ tests/lean/have.lean.expected.out | 8 +++++++- 3 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index de40ac3e00..04b1cba729 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -546,13 +546,13 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va if useLetExpr then withLetDecl id.getId type val fun x => do addLocalVarInfo id x - let body ← elabTerm body expectedType? + let body ← elabTermEnsuringType body expectedType? let body ← instantiateMVars body mkLetFVars #[x] body else let f ← withLocalDecl id.getId BinderInfo.default type fun x => do addLocalVarInfo id x - let body ← elabTerm body expectedType? + let body ← elabTermEnsuringType body expectedType? let body ← instantiateMVars body mkLambdaFVars #[x] body pure <| mkApp f val diff --git a/tests/lean/have.lean b/tests/lean/have.lean index a912c22107..153d8b88ca 100644 --- a/tests/lean/have.lean +++ b/tests/lean/have.lean @@ -1,2 +1,7 @@ example : False := have False := _ + +example : 5 = 3 := + have t : True := _ + have f : 5 = 6 := _ + f diff --git a/tests/lean/have.lean.expected.out b/tests/lean/have.lean.expected.out index 8990ee34bb..d8be69cbef 100644 --- a/tests/lean/have.lean.expected.out +++ b/tests/lean/have.lean.expected.out @@ -1,4 +1,10 @@ -have.lean:3:0: error: unexpected end of input +have.lean:4:0: error: expected term have.lean:2:16-2:17: error: don't know how to synthesize placeholder context: ⊢ False +have.lean:7:2-7:3: error: type mismatch + f +has type + 5 = 6 : Prop +but is expected to have type + 5 = 3 : Prop