2024-02-23から1日間の記事一覧
TaPL24章のネタです。まずStatementがcoqで正しく書けているか怪しいですが… Theorem exists_forall_second: forall T: Prop -> Prop, ((exists X, T X) <-> (forall Y: Prop, (forall X, T X -> Y) -> Y)). intros. split. - intros. destruct H. now apply…
TaPL24章のネタです。まずStatementがcoqで正しく書けているか怪しいですが… Theorem exists_forall_second: forall T: Prop -> Prop, ((exists X, T X) <-> (forall Y: Prop, (forall X, T X -> Y) -> Y)). intros. split. - intros. destruct H. now apply…