chore: HasRepr ==> Repr

src/Init/Control/EState.lean

@@ -22,7 +22,7 @@ instance [ToString ε] [ToString α] : ToString (Result ε σ α) := {
     | Result.error e _ => "error: " ++ toString e
 }
 
-instance [HasRepr ε] [HasRepr α] : HasRepr (Result ε σ α) := {
+instance [Repr ε] [Repr α] : Repr (Result ε σ α) := {
   repr := fun
     | Result.error e _ => "(error " ++ repr e ++ ")"
     | Result.ok a _    => "(ok " ++ repr a ++ ")"

src/Init/Control/Except.lean

@@ -30,12 +30,12 @@ protected def Except.toString [ToString ε] [ToString α] : Except ε α → Str
   | Except.error e => "(error " ++ toString e ++ ")"
   | Except.ok a    => "(ok " ++ toString a ++ ")"
 
-protected def Except.repr [HasRepr ε] [HasRepr α] : Except ε α → String
+protected def Except.repr [Repr ε] [Repr α] : Except ε α → String
   | Except.error e => "(error " ++ repr e ++ ")"
   | Except.ok a    => "(ok " ++ repr a ++ ")"
 
 instance [ToString ε] [ToString α] : ToString (Except ε α) := ⟨Except.toString⟩
-instance [HasRepr ε] [HasRepr α] : HasRepr (Except ε α) := ⟨Except.repr⟩
+instance [Repr ε] [Repr α] : Repr (Except ε α) := ⟨Except.repr⟩
 end
 
 namespace Except

src/Init/Data/Array/Basic.lean

@@ -437,7 +437,7 @@ a.foldlStep (fun r a => Array.push r a) empty 2
 def toList (a : Array α) : List α :=
 a.foldr List.cons []
 
-instance [HasRepr α] : HasRepr (Array α) :=
+instance [Repr α] : Repr (Array α) :=
 ⟨fun a => "#" ++ repr a.toList⟩
 
 instance [ToString α] : ToString (Array α) :=

src/Init/Data/Int/Basic.lean

@@ -122,7 +122,7 @@ protected def repr : Int → String
   | ofNat m   => Nat.repr m
   | negSucc m => "-" ++ Nat.repr (succ m)
 
-instance : HasRepr Int := ⟨Int.repr⟩
+instance : Repr Int := ⟨Int.repr⟩
 instance : ToString Int := ⟨Int.repr⟩
 instance : HasOfNat Int := ⟨Int.ofNat⟩
 

src/Init/Data/Random.lean

@@ -37,7 +37,7 @@ instance : Inhabited StdGen := ⟨{ s1 := 0, s2 := 0 }⟩
 
 def stdRange := (1, 2147483562)
 
-instance : HasRepr StdGen := {
+instance : Repr StdGen := {
   repr := fun ⟨s1, s2⟩ => "⟨" ++ toString s1 ++ ", " ++ toString s2 ++ "⟩"
 }
 

src/Init/Data/Repr.lean

@@ -12,61 +12,61 @@ open Sum Subtype Nat
 
 universes u v
 
-class HasRepr (α : Type u) :=
+class Repr (α : Type u) :=
   (repr : α → String)
 
-export HasRepr (repr)
+export Repr (repr)
 
 -- This instance is needed because `id` is not reducible
-instance {α : Type u} [HasRepr α] : HasRepr (id α) :=
-  inferInstanceAs (HasRepr α)
+instance {α : Type u} [Repr α] : Repr (id α) :=
+  inferInstanceAs (Repr α)
 
-instance : HasRepr Bool :=
+instance : Repr Bool :=
   ⟨fun b => cond b "true" "false"⟩
 
-instance {α} [HasRepr α] : HasRepr (Id α) :=
-  inferInstanceAs (HasRepr α)
+instance {α} [Repr α] : Repr (Id α) :=
+  inferInstanceAs (Repr α)
 
-instance {p : Prop} : HasRepr (Decidable p) := {
+instance {p : Prop} : Repr (Decidable p) := {
   repr := fun h => match h with
   | Decidable.isTrue _  => "true"
   | Decidable.isFalse _ => "false"
 }
 
-protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String
+protected def List.reprAux {α : Type u} [Repr α] : Bool → List α → String
   | b,     []    => ""
   | true,  x::xs => repr x ++ List.reprAux false xs
   | false, x::xs => ", " ++ repr x ++ List.reprAux false xs
 
-protected def List.repr {α : Type u} [HasRepr α] : List α → String
+protected def List.repr {α : Type u} [Repr α] : List α → String
   | []    => "[]"
   | x::xs => "[" ++ List.reprAux true (x::xs) ++ "]"
 
-instance {α : Type u} [HasRepr α] : HasRepr (List α) :=
+instance {α : Type u} [Repr α] : Repr (List α) :=
   ⟨List.repr⟩
 
-instance : HasRepr PUnit.{u+1} :=
+instance : Repr PUnit.{u+1} :=
   ⟨fun u => "PUnit.unit"⟩
 
-instance {α : Type u} [HasRepr α] : HasRepr (ULift.{v} α) :=
+instance {α : Type u} [Repr α] : Repr (ULift.{v} α) :=
   ⟨fun v => "ULift.up (" ++ repr v.1 ++ ")"⟩
 
-instance : HasRepr Unit :=
+instance : Repr Unit :=
   ⟨fun u => "()"⟩
 
-instance {α : Type u} [HasRepr α] : HasRepr (Option α) :=
+instance {α : Type u} [Repr α] : Repr (Option α) :=
   ⟨fun | none => "none" | (some a) => "(some " ++ repr a ++ ")"⟩
 
-instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (Sum α β) :=
+instance {α : Type u} {β : Type v} [Repr α] [Repr β] : Repr (Sum α β) :=
   ⟨fun | (inl a) => "(inl " ++ repr a ++ ")" | (inr b) => "(inr " ++ repr b ++ ")"⟩
 
-instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (α × β) :=
+instance {α : Type u} {β : Type v} [Repr α] [Repr β] : Repr (α × β) :=
   ⟨fun ⟨a, b⟩ => "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩
 
-instance {α : Type u} {β : α → Type v} [HasRepr α] [s : ∀ x, HasRepr (β x)] : HasRepr (Sigma β) :=
+instance {α : Type u} {β : α → Type v} [Repr α] [s : ∀ x, Repr (β x)] : Repr (Sigma β) :=
   ⟨fun ⟨a, b⟩ => "⟨"  ++ repr a ++ ", " ++ repr b ++ "⟩"⟩
 
-instance {α : Type u} {p : α → Prop} [HasRepr α] : HasRepr (Subtype p) :=
+instance {α : Type u} {p : α → Prop} [Repr α] : Repr (Subtype p) :=
   ⟨fun s => repr (val s)⟩
 
 namespace Nat
@@ -132,7 +132,7 @@ def toSuperscriptString (n : Nat) : String :=
 
 end Nat
 
-instance : HasRepr Nat :=
+instance : Repr Nat :=
   ⟨Nat.repr⟩
 
 def hexDigitRepr (n : Nat) : String :=
@@ -152,29 +152,29 @@ def Char.quoteCore (c : Char) : String :=
   else if  c.toNat <= 31 ∨ c = '\x7f' then "\\x" ++ charToHex c
   else String.singleton c
 
-instance : HasRepr Char :=
+instance : Repr Char :=
   ⟨fun c => "'" ++ Char.quoteCore c ++ "'"⟩
 
 def String.quote (s : String) : String :=
   if s.isEmpty = true then "\"\""
   else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\""
 
-instance : HasRepr String :=
+instance : Repr String :=
   ⟨String.quote⟩
 
-instance : HasRepr Substring :=
+instance : Repr Substring :=
   ⟨fun s => String.quote s.toString ++ ".toSubstring"⟩
 
-instance : HasRepr String.Iterator :=
+instance : Repr String.Iterator :=
   ⟨fun ⟨s, pos⟩ => "(String.Iterator.mk " ++ repr s ++ " " ++ repr pos ++ ")"⟩
 
-instance (n : Nat) : HasRepr (Fin n) :=
+instance (n : Nat) : Repr (Fin n) :=
   ⟨fun f => repr (Fin.val f)⟩
 
-instance : HasRepr UInt16 := ⟨fun n => repr n.toNat⟩
-instance : HasRepr UInt32 := ⟨fun n => repr n.toNat⟩
-instance : HasRepr UInt64 := ⟨fun n => repr n.toNat⟩
-instance : HasRepr USize  := ⟨fun n => repr n.toNat⟩
+instance : Repr UInt16 := ⟨fun n => repr n.toNat⟩
+instance : Repr UInt32 := ⟨fun n => repr n.toNat⟩
+instance : Repr UInt64 := ⟨fun n => repr n.toNat⟩
+instance : Repr USize  := ⟨fun n => repr n.toNat⟩
 
 protected def Char.repr (c : Char) : String :=
   repr c

src/Init/System/IO.lean

@@ -468,7 +468,7 @@ class HasEval (α : Type u) :=
   -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbgTrace!`)
   (eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit)
 
-instance {α : Type u} [HasRepr α] : HasEval α :=
+instance {α : Type u} [Repr α] : HasEval α :=
   ⟨fun a _ => IO.println (repr (a ()))⟩
 
 instance : HasEval Unit :=

src/Lean/Data/Format.lean

@@ -273,7 +273,7 @@ protected def Format.repr : Format → Format
 
 instance : ToString Format := ⟨Format.pretty⟩
 
-instance : HasRepr Format := ⟨Format.pretty ∘ Format.repr⟩
+instance : Repr Format := ⟨Format.pretty ∘ Format.repr⟩
 
 def formatDataValue : DataValue → Format
   | DataValue.ofString v => format (repr v)

src/Lean/Data/Json/Basic.lean

@@ -73,7 +73,7 @@ protected def shiftr : JsonNumber → Nat → JsonNumber
 
 instance : ToString JsonNumber := ⟨JsonNumber.toString⟩
 
-instance : HasRepr JsonNumber :=
+instance : Repr JsonNumber :=
   ⟨fun ⟨m, e⟩ => "⟨" ++ m.repr ++ "," ++ e.repr ++ "⟩"⟩
 
 end JsonNumber

src/Lean/Expr.lean

@@ -682,7 +682,7 @@ def replaceFVars (e : Expr) (fvars : Array Expr) (vs : Array Expr) : Expr :=
 instance : ToString Expr := ⟨Expr.dbgToString⟩
 
 -- TODO: should not use dbgToString, but constructors.
-instance : HasRepr Expr := ⟨Expr.dbgToString⟩
+instance : Repr Expr := ⟨Expr.dbgToString⟩
 
 def isAtomic : Expr → Bool
   | Expr.const _ _ _ => true
@@ -738,7 +738,7 @@ instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩
 instance : HasBeq ExprStructEq := ⟨ExprStructEq.beq⟩
 instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩
 instance : ToString ExprStructEq := ⟨fun e => toString e.val⟩
-instance : HasRepr ExprStructEq := ⟨fun e => repr e.val⟩
+instance : Repr ExprStructEq := ⟨fun e => repr e.val⟩
 
 end ExprStructEq
 

src/Std/Data/RBMap.lean

@@ -257,7 +257,7 @@ def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat :=
     | some ⟨k, v⟩ => some (k, v)
     | none        => none
 
-instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) :=
+instance [Repr α] [Repr β] : Repr (RBMap α β lt) :=
   ⟨fun t => "rbmapOf " ++ repr t.toList⟩
 
 @[inline] def insert : RBMap α β lt → α → β → RBMap α β lt

src/Std/Data/RBTree.lean

@@ -53,7 +53,7 @@ variables {α : Type u} {β : Type v} {lt : α → α → Bool}
   | some ⟨a, _⟩ => some a
   | none        => none
 
-instance [HasRepr α] : HasRepr (RBTree α lt) :=
+instance [Repr α] : Repr (RBTree α lt) :=
   ⟨fun t => "rbtreeOf " ++ repr t.toList⟩
 
 @[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt :=

tests/bench/rbmap3.lean

@@ -206,7 +206,7 @@ t.val.depth f
   | some ⟨k, v⟩ => some (k, v)
   | none        => none
 
-instance [HasRepr α] [HasRepr β] : HasRepr (Rbmap α β lt) :=
+instance [Repr α] [Repr β] : Repr (Rbmap α β lt) :=
 ⟨fun t => "rbmapOf " ++ repr t.toList⟩
 
 variables [DecidableRel lt]

tests/lean/repr_issue.lean

@@ -12,6 +12,6 @@ def ex₂ : ExceptT String (StateT (Array Nat) Id) Nat :=
 foo
 
 -- The following examples were producing an element of Type `id (Except String Nat)`.
--- Type class resolution was failing to produce an instance for `HasRepr (id (Except String Nat))` because `id` is not transparent.
+-- Type class resolution was failing to produce an instance for `Repr (id (Except String Nat))` because `id` is not transparent.
 #eval ex₁.run' (mkArray 10 1000) $.run
 #eval ex₂.run' (mkArray 10 1000) $.run

tests/lean/run/125.lean

@@ -17,7 +17,7 @@ match foo with
 | mk1 b => s!"OH {b}"
 | mk2 b => s!"DR {b}"
 
-instance : HasRepr Foo := ⟨fooRepr⟩
+instance : Repr Foo := ⟨fooRepr⟩
 
 #eval elems Foo
 

tests/lean/run/IO_test.lean

@@ -6,9 +6,9 @@ import Init.Data.ToString
 
 open IO.FS
 
-instance : HasRepr UInt8 := ⟨ toString ⟩
+instance : Repr UInt8 := ⟨ toString ⟩
 
-def check_eq {α} [HasBeq α] [HasRepr α] (tag : String) (expected actual : α) : IO Unit :=
+def check_eq {α} [HasBeq α] [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

@@ -5,7 +5,7 @@ structure MyState :=
 (bs : Nat := 0) -- backtrackable state
 (ps : Nat := 0) -- non backtrackable state
 
-instance : HasRepr MyState :=
+instance : Repr MyState :=
 ⟨fun s => repr (s.bs, s.ps)⟩
 
 instance : EStateM.Backtrackable Nat MyState :=