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.

此博客中的热门博文

少写代码,多读别人写的代码

在windows下使用llvm+clang

tensorflow distributed runtime初窥