2010-02-04から1日間の記事一覧
概要 Coqの些末な話。 proj2_sigの定義が読めなかったのでletについて調べた。 (* proj2_sig = fun (A : Type) (P : A -> Prop) (e : sig P) => let (a, b) as e0 return (P (proj1_sig e0)) := e in b : forall (A : Type) (P : A -> Prop) (e : sig P), P …
概要 Coqの些末な話。 proj2_sigの定義が読めなかったのでletについて調べた。 (* proj2_sig = fun (A : Type) (P : A -> Prop) (e : sig P) => let (a, b) as e0 return (P (proj1_sig e0)) := e in b : forall (A : Type) (P : A -> Prop) (e : sig P), P …