data D : Set0 -> Set0 where nat : D Nat bool : D Bool f : {A : Set0} -> A -> D A -> Unit f (zero) (nat) = unit Cannot split on argument of non-datatype @0 when checking the definition of f これは、Agda2のnotesディレクトリの中、"inductive-f…

data Nat : Set0 where zero : Nat succ : Nat -> Nat data Ty {A : Set0} : A -> Set0 where ty : (a : A) -> Ty a f : Ty zero -> Nat f (ty .zero) = zero {- f (ty zero) = zeroだとすると a != zero of type Nat when checking that the pattern ty zer…

昨日のアレはMLで質問してみました http://thread.gmane.org/gmane.comp.lang.agda/1015すると、Wouterさんが、 http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.DatatypeAndFunctionDefinitions ここにdot patternがあるからそれを使えば良いんじゃね…