chore: fix tests

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
 

tests/lean/repr_issue.lean.expected.out

@@ -1,2 +1,2 @@
-(ok 1000)
-(ok 33)
+Except.ok 1000
+Except.ok 33

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
 

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}"

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,

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