2009-05-28 分かっているけれどつらい話 Agda Agdaでは、postulateで与えられた A : Set に対し、f : A -> Boolを定義した際、任意の t: A にたいし、 : Bool (ただし xがtに登場することを とここでは表記している)を定義することが出来ない。構成的型理論としては当たり前だけれど、やっぱり不便だ。