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

fix: error position

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-21 16:09:24 +01:00
parent 772e62dfaa
commit 3e77c7cdef
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/Do.lean
View file

@ -216,7 +216,7 @@ def hasBreakContinueReturn (c : Code) : Bool :=
| Code.«return» _ _ => true
| _ => false
def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax → m Code) : m Code := withFreshMacroScope do
def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax → m Code) : m Code := withRef e <| withFreshMacroScope do
let y ← `(y)
let yName := y.getId
let doElem ← `(doElem| let y ← $e:term)

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

@ -19,7 +19,7 @@ match1.lean:113:0: error: dependent match elimination failed, inaccessible patte
.(j + j)
constructor expected
[false, true, true]
match1.lean:124:0: error: invalid match-expression, type of pattern variable 'a' contains metavariables
match1.lean:124:7: error: invalid match-expression, type of pattern variable 'a' contains metavariables
?m
fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m
fun (x : Nat × Nat) =>