2009-09-15から1日間の記事一覧
髪の毛が乾くまで暇なので書く。 data Unit : Set0 where unit : Unit data Ty : Unit -> Set0 where ty : (u : Unit) -> Ty u f : (Ty unit) -> Unit f (ty unit) = unit g : Ty unit -> Unit g (ty x) = unit この型チェックエラーメッセージ fの型チェッ…
髪の毛が乾くまで暇なので書く。 data Unit : Set0 where unit : Unit data Ty : Unit -> Set0 where ty : (u : Unit) -> Ty u f : (Ty unit) -> Unit f (ty unit) = unit g : Ty unit -> Unit g (ty x) = unit この型チェックエラーメッセージ fの型チェッ…