2009-09-12から1日間の記事一覧
data Unit : Set0 where unit : Unit data Ty : Unit -> Set0 where ty : (u : Unit) -> Ty u f : Ty unit -> Unit f (ty unit) = unit g : Ty unit -> Unit g (ty a) = agがあれだよなー a != unit of type Unit when checking that the pattern ty a has t…