From 92f0afa424e79ff1891bdb0420ee386e6af02321 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 18 Dec 2020 11:11:04 -0800
Subject: [PATCH] chore: fix tests

---
 src/Init/Data/Repr.lean                  |  3 +++
 tests/lean/repr_issue.lean.expected.out  |  4 ++--
 tests/lean/run/125.lean                  | 10 ++++------
 tests/lean/run/IO_test.lean              |  2 --
 tests/lean/run/backtrackable_estate.lean |  8 ++++----
 tests/lean/string_imp.lean.expected.out  |  2 +-
 6 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 49aa469f6c..d814697d19 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -209,6 +209,9 @@ instance : Repr String.Iterator where
 instance (n : Nat) : Repr (Fin n) where
   reprPrec f _ := repr f.val
 
+instance : Repr UInt8 where
+  reprPrec n _ := repr n.toNat
+
 instance : Repr UInt16 where
   reprPrec n _ := repr n.toNat
 
diff --git a/tests/lean/repr_issue.lean.expected.out b/tests/lean/repr_issue.lean.expected.out
index 1e7e4f8c81..67a421a1ba 100644
--- a/tests/lean/repr_issue.lean.expected.out
+++ b/tests/lean/repr_issue.lean.expected.out
@@ -1,2 +1,2 @@
-(ok 1000)
-(ok 33)
+Except.ok 1000
+Except.ok 33
diff --git a/tests/lean/run/125.lean b/tests/lean/run/125.lean
index c24fb615b8..afa97f6a23 100644
--- a/tests/lean/run/125.lean
+++ b/tests/lean/run/125.lean
@@ -1,5 +1,3 @@
-
-
 class HasElems (α : Type) : Type := (elems : Array α)
 def elems (α : Type) [HasElems α] : Array α := HasElems.elems
 
@@ -13,11 +11,11 @@ instance BoolElems : HasElems Bool := ⟨#[false, true]⟩
 instance FooElems  : HasElems Foo  := ⟨(elems Bool).map mk1 ++ (elems Bool).map mk2⟩
 
 def fooRepr (foo : Foo) :=
-match foo with
-| mk1 b => s!"OH {b}"
-| mk2 b => s!"DR {b}"
+  match foo with
+  | mk1 b => f!"OH {b}"
+  | mk2 b => f!"DR {b}"
 
-instance : Repr Foo := ⟨fooRepr⟩
+instance : Repr Foo := ⟨fun s _ => fooRepr s⟩
 
 #eval elems Foo
 
diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean
index 0157e42777..f22c4f558e 100644
--- a/tests/lean/run/IO_test.lean
+++ b/tests/lean/run/IO_test.lean
@@ -6,8 +6,6 @@ import Init.Data.ToString
 
 open IO.FS
 
-instance : Repr UInt8 := ⟨ toString ⟩
-
 def check_eq {α} [BEq α] [Repr α] (tag : String) (expected actual : α) : IO Unit :=
 «unless» (expected == actual) $ throw $ IO.userError $
   s!"assertion failure \"{tag}\":\n  expected: {repr expected}\n  actual:   {repr actual}"
diff --git a/tests/lean/run/backtrackable_estate.lean b/tests/lean/run/backtrackable_estate.lean
index 653dbc3e06..113adcc3c8 100644
--- a/tests/lean/run/backtrackable_estate.lean
+++ b/tests/lean/run/backtrackable_estate.lean
@@ -2,11 +2,11 @@ import Init.System.IO
 
 
 structure MyState :=
-(bs : Nat := 0) -- backtrackable state
-(ps : Nat := 0) -- non backtrackable state
+  bs : Nat := 0 -- backtrackable state
+  ps : Nat := 0 -- non backtrackable state
 
-instance : Repr MyState :=
-⟨fun s => repr (s.bs, s.ps)⟩
+instance : Repr MyState where
+  reprPrec s _ := repr (s.bs, s.ps)
 
 instance : EStateM.Backtrackable Nat MyState :=
 { save    := fun s => s.bs,
diff --git a/tests/lean/string_imp.lean.expected.out b/tests/lean/string_imp.lean.expected.out
index 53ed150410..242d7759ff 100644
--- a/tests/lean/string_imp.lean.expected.out
+++ b/tests/lean/string_imp.lean.expected.out
@@ -5,5 +5,5 @@
 0
 2
 4
-(String.Iterator.mk "αacc" 2)
+String.Iterator.mk "αacc" 2
 6