From 82780be1442f65cd7954a367674ba1e4afe367b7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jun 2020 18:49:44 -0700 Subject: [PATCH] chore: fix tests --- tests/lean/appParserIssue.lean.expected.out | 10 +++++----- tests/lean/phashmap_inst_coherence.lean.expected.out | 4 ++-- tests/lean/precissues.lean.expected.out | 12 ++++++------ 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/tests/lean/appParserIssue.lean.expected.out b/tests/lean/appParserIssue.lean.expected.out index 5159445430..8cf79557da 100644 --- a/tests/lean/appParserIssue.lean.expected.out +++ b/tests/lean/appParserIssue.lean.expected.out @@ -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 diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out index ea7b2e3c5e..32f2b65b3a 100644 --- a/tests/lean/phashmap_inst_coherence.lean.expected.out +++ b/tests/lean/phashmap_inst_coherence.lean.expected.out @@ -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 diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out index 7af92953dd..3e18692258 100644 --- a/tests/lean/precissues.lean.expected.out +++ b/tests/lean/precissues.lean.expected.out @@ -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