ハロー、依存型プログラミングの世界 (2) データ型の宣言 代数データ型を宣言する場合には、Haskellと同様の記法を使うことができる。HaskellでもおなじみのEitherやListの宣言はidrisではこうなっている。 data Either a b = Left a | Right b data List a …