Coq中手动证明简单的逻辑命题

Section MiniPropLogic.
Variables P Q R T : Prop.
Theorem imp_trans : (P->Q)->(Q->R)->P->R.
Proof.
intros H H' p.
apply H'.
apply H.
assumption.
Qed.
End MiniPropLogic.

评论

此博客中的热门博文

想换个新路由器

这几天玩快手玩的入迷

用java生tensorflow的tfrecord文件