chore(tests): add Leo's test case for errors in solve1-blocks
This commit is contained in:
parent
54114fd7bd
commit
5d6bf38b7e
2 changed files with 13 additions and 0 deletions
|
|
@ -45,3 +45,11 @@ begin
|
|||
{ subst h1 },
|
||||
--^ error should be at `}`
|
||||
end
|
||||
|
||||
example : true :=
|
||||
begin
|
||||
{
|
||||
note h' := eq.refl _,
|
||||
--^ error should be on this line
|
||||
}
|
||||
end
|
||||
|
|
@ -42,3 +42,8 @@ state:
|
|||
b : ℕ,
|
||||
h2 : b = 0
|
||||
⊢ 0 = b
|
||||
auto_quote_error2.lean:52:15: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
⊢ Sort ?
|
||||
state:
|
||||
⊢ true
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue