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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-17 18:49:44 -07:00
parent 196435c73b
commit 82780be144
3 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
tests/lean/appParserIssue.lean.expected.out
View file

@ -1,5 +1,5 @@
f 1 (λ (x : Nat), x) : Nat
f 1 (λ (x : Nat), x) : Nat
f 1 (λ (x : Nat), x) : Nat
f 1 (λ (x : Nat), x) : Nat
f 1 (λ (x : Nat), x) : Nat
f 1 (fun (x : Nat) => x) : Nat
f 1 (fun (x : Nat) => x) : Nat
f 1 (fun (x : Nat) => x) : Nat
f 1 (fun (x : Nat) => x) : Nat
f 1 (fun (x : Nat) => x) : Nat

4
tests/lean/phashmap_inst_coherence.lean.expected.out
View file

@ -3,6 +3,6 @@ phashmap_inst_coherence.lean:11:0: error: type mismatch at application
term
m
has type
@PersistentHashMap Nat Nat (@beqOfEq Nat (λ (ab : Nat), Nat.DecidableEq a b)) Nat.Hashable
@PersistentHashMap Nat Nat (@beqOfEq Nat (fun (ab : Nat) => Nat.DecidableEq a b)) Nat.Hashable
but is expected to have type
@PersistentHashMap Nat Nat (@beqOfEq Nat (λ (ab : Nat), Nat.DecidableEq a b)) natDiffHash
@PersistentHashMap Nat Nat (@beqOfEq Nat (fun (ab : Nat) => Nat.DecidableEq a b)) natDiffHash

12
tests/lean/precissues.lean.expected.out
View file

@ -1,14 +1,14 @@
id (λ (x : ?m_1), x) : ?m_1 → ?m_1
id (fun (x : ?m_1) => x) : ?m_1 → ?m_1
0 : Nat
f 1 (λ (x : Nat), x) : Nat
f 1 (fun (x : Nat) => x) : Nat
0 : Nat
f 1 (λ (x : Nat), x) : Nat
f 1 (fun (x : Nat) => x) : Nat
id : ?m_1 → ?m_1
precissues.lean:15:10: error: expected command
1 : Nat
id ((λ (this : True), this) True.intro) : True
0=(λ (this : Nat), this) 1 : Prop
0=let x : Nat := 0; x : Prop
id ((fun (this : True) => this) True.intro) : True
0=(fun (this : Nat) => this) 1 : Prop
0=let x : Nat := 0 in x : Prop
p↔¬q : Prop
True=¬False : Prop
p∧¬q : Prop