Require Import String. Open Scope string_scope. (* 型クラスShowの定義 *) Class Show (A: Set) := { show : A -> string }. (* フィールドshowの型 *) Check @show. (* show : forall A : Set, Show A -> A -> string ((A:Set)と(s:Show A)の部分は暗黙引数となり、省略可能) *) (* string型をShowクラスのインスタンスとする *) Instance ShowString : Show string := { show s := s }. (* bool型をShowクラスのインスタンスとする *) Instance ShowBool : Show bool := { show b := match b