2009-09-16から1日間の記事一覧
Inductive Bool : Set := true : Bool | false : Bool. Inductive Ty {A : Set} : A -> Set := ty (a : A) : Ty a. Definition f (arg : Ty true) := match arg with | ty true => true end. これで、fをCheckすると f : Ty true -> match true with | true …