#instances

#instances は、与えられた型クラスのインスタンスの完全なリストを出力するコマンドです。

import Batteries.Tactic.Instances -- `#instances` コマンドを使うために必要

-- 内容が何もない例示のためだけの型クラス
class Hoge (α : Type) where
  hoge : Unit

-- `Nat` を `Hoge` のインスタンスにする
instance : Hoge Nat where
  hoge := ()

-- `Bool` を `Hoge` のインスタンスにする
instance : Hoge Bool where
  hoge := ()

-- 今登録した2つのインスタンスが表示される
/-
info: 2 instances:

instHogeBool : Hoge Bool
instHogeNat : Hoge Nat
-/
#instances Hoge