chore: fix tests

This commit is contained in:
Leonardo de Moura 2021-04-03 18:24:03 -07:00
parent 09ee8bddad
commit 750691bd5a
3 changed files with 8 additions and 6 deletions

View file

@ -166,6 +166,8 @@
| (z, w) =>
let z1 : Nat := z + w;
z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩
[.] `z : none
[.] `w : none
(z, w) : Nat × Nat @ ⟨23, 8⟩-⟨23, 14⟩
Macro expansion
(z, w)

View file

@ -1,15 +1,15 @@
namedHoles.lean:9:7-9:14: error: application type mismatch
f ?m ?m
f ?x ?x
argument
?m
?x
has type
Nat : Type
but is expected to have type
Bool : Type
g ?m ?m : Nat
g ?x ?x : Nat
20
foo (fun (x : Nat) => ?m x) ?m : Nat
bla ?m fun (x : Nat) => ?m : Nat
foo (fun (x : Nat) => ?m x) ?hole : Nat
bla ?hole fun (x : Nat) => ?hole : Nat
namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
boo (fun (x : Nat) => ?m x) fun (y : Bool) => sorry : Nat
11

View file

@ -2,7 +2,7 @@
as bs : List α
⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
rewrite.lean:12:20-12:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
List.reverse (List.reverse ?m)
List.reverse (List.reverse ?as)
α : Type u_1
as bs : List α
⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)