2009-10-23から1日間の記事一覧
{-# LANGUAGE GADTs #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE KindSignatures #-} data Zero data Succ a data Plus a b data Id :: * -> * -> * where Refl :: a -> Id a a Symm :: (Id a b) -> Id b a Tran :: (Id a b) -> (Id b c) -> (Id a c)…