Repr

Repr は，その型の項をどのように表示するかを指示する型クラスです．

たとえば，以下のように新しく構造体 Point を定義したとき，特に何も指定しなければ Point の項を #eval で表示することはできません．

-- 平面上の点を表す構造体
structure Point (α : Type) : Type where
  x : α
  y : α

-- 原点
def origin : Point Nat := ⟨0, 0⟩

/--
error: expression
  origin
has type
  Point Nat
but instance
  Lean.Eval (Point Nat)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
-/
#eval origin

エラーメッセージが示すように，これは Point が型クラス Lean.Eval のインスタンスではないからです．エラーメッセージには，Repr クラスのインスタンスであれば自動的に Lean.Eval のインスタンスにもなることが書かれています．通常，Lean.Eval のインスタンスを手で登録することはなく，Repr インスタンスによって自動生成させます．

Repr インスタンスの登録方法ですが，通り一遍の表示で構わなければ deriving コマンドで Lean に自動生成させることができます．

deriving instance Repr for Point

#eval origin

あるいは，Point の定義時に以下のようにしても構いません．

structure Point (α : Type) : Type where
  x : α
  y : α
deriving Repr

def origin : Point Nat := ⟨0, 0⟩

#eval origin