Coqで型クラス - Qiita

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

[minamiyama1994]

ん？　これShow stringの定義違うくないか、"hello"は"\"hello\""になるべきでは #細かい