Haskellの話じゃなくて、またもAgda2の話です。具体的には data Nat : Set0 where zero : Nat succ : Nat -> Nat data Bool : Set0 where true : Bool false : Boolとかでまぁ、データ型を定義して、その上で次のような関数 nonsense : Set0 -> Nat nonsense…

分からなくなるもなにも、最初から何も知らん！！！！！！！ data Bool :: * where true :: Bool false :: Bool みたいな事を書いた時、このtrueとかfalseさんて一体何者なんだろうっていう雰囲気。例えば、 data Bool :: * where true :: Nat false :: Nat …