2008-06-02から1日間の記事一覧
例としてand除去を含む証明。 Coq < Goal forall A B : Prop, A /\ B -> B. ... Unnamed_thm < intros. 1 subgoal A : Prop B : Prop H : A /\ B ============================ B Unnamed_thm < elim H. 1 subgoal A : Prop B : Prop H : A /\ B ===========…
例としてand除去を含む証明。 Coq < Goal forall A B : Prop, A /\ B -> B. ... Unnamed_thm < intros. 1 subgoal A : Prop B : Prop H : A /\ B ============================ B Unnamed_thm < elim H. 1 subgoal A : Prop B : Prop H : A /\ B ===========…
