Coqで型クラス

Last updated at 2013-10-26Posted at 2012-12-26

Show.v

RequireImportString.OpenScopestring_scope.(* 型クラスShowの定義 *)ClassShow(A:Set):={show:A->string}.(* フィールドshowの型 *)Check@show.(*
show
 : forall A : Set, Show A -> A -> string
((A:Set)と(s:Show A)の部分は暗黙引数となり、省略可能)
*)(* string型をShowクラスのインスタンスとする *)InstanceShowString:Showstring:={shows:=s}.(* bool型をShowクラスのインスタンスとする *)InstanceShowBool:Showbool:={showb:=matchbwith|true=>"true"|false=>"false"end}.(* 文字列はShowクラスのインスタンス *)Definitionfoo:=show"hello".(* ブール型はShowクラスのインスタンス *)Definitionbar:=showtrue.(* 混ぜても使える *)Definitionhoge:=show"hello"++showfalse.

Go to list of users who liked

Go to list of comments

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

URL: https://qiita.com/yoshihiro503/items/a6fe93ae0d867129f7b1

⇱ Coqで型クラス #class - Qiita

Coqで型クラス