From a5cf1ac5ae0fd5eec1dd751074b8068b3230d043 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Nov 2019 18:07:13 -0800 Subject: [PATCH] chore: fix tests --- tests/compiler/strictOrSimp.lean | 2 +- tests/lean/phashmap_inst_coherence.lean.expected.out | 4 ++-- tests/lean/trust0/basic.lean | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/compiler/strictOrSimp.lean b/tests/compiler/strictOrSimp.lean index f8c349a6e9..ea135c5015 100644 --- a/tests/compiler/strictOrSimp.lean +++ b/tests/compiler/strictOrSimp.lean @@ -8,4 +8,4 @@ if strictOr (C == 0) (spin b) then "hello" else "world" def main (xs : List String) : IO Unit := -IO.println (f xs.head!.toNat) +IO.println (f 0) diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out index 213a41dd01..6cf09f3e51 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 Nat.Hashable (@beqOfEq Nat Nat.DecidableEq) + @PersistentHashMap Nat Nat Nat.Hashable (@beqOfEq Nat (λ (ab : Nat), Nat.DecidableEq a b)) but is expected to have type - @PersistentHashMap Nat Nat natDiffHash (@beqOfEq Nat Nat.DecidableEq) + @PersistentHashMap Nat Nat natDiffHash (@beqOfEq Nat (λ (ab : Nat), Nat.DecidableEq a b)) diff --git a/tests/lean/trust0/basic.lean b/tests/lean/trust0/basic.lean index f6234d76ae..ec1dba0fe2 100644 --- a/tests/lean/trust0/basic.lean +++ b/tests/lean/trust0/basic.lean @@ -62,7 +62,7 @@ def hasDecEq : ∀ (a b : Nat), Decidable (a = b) | isFalse xney => isFalse (fun h => Nat.noConfusion h (fun xeqy => absurd xeqy xney)) instance : DecidableEq ℕ := -{decEq := hasDecEq} +hasDecEq def repeat.{u} {α : Type u} (f : ℕ → α → α) : ℕ → α → α | 0, a => a