2010-09-21から1日間の記事一覧
Inductive eq {Ty : Set} : Ty -> Ty -> Set := | Refl : forall v , eq v v. Inductive sgl {Ty : Set} : Ty -> Set := | Sgl : forall v , sgl v. Definition test {ts ts' : nat} (obj : eq ts ts') (s : sgl ts) : sgl ts' := match obj with | Refl v =…