coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: guninski AT guninski.com
- To: coq-club AT inria.fr
- Subject: [Coq-Club]
- Date: Sun, 8 May 2011 17:44:41 +0200
is this logical implication:
Lemma lv: Type->True. Proof. intuition. Qed.
Coq < Print lv.
lv = fun _ : Type => I
: Type -> True
Argument scope is [type_scope]
- [Coq-Club], guninski
Archive powered by MhonArc 2.6.16.