copatterns概要 - ぼくのぬまち 出張版ghc-7.8でビルドできるAgdaマダカナーとか思いつつ，Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら，実験的機能としてcopatternsってやつが入ると書かれている．余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつつ読むと，なにやらこんなカンジのようだ． タプルをレコードで定義すると，次のようになる． record _×_ (A B : Set) : Set where constructor _,_ field fst : A snd : B open _×_タプルのフィールドとしては1番目の要素であるfstと2番目の要素であるsndを持っていて，recordをopenすればこれらは普通に関数として使える． 通常，タプルを与えるような関数は最終的にタプルをコンストラクトすることになる． pair : {A B : Set} →
