coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jeffrey Terrell <jeffrey.terrell AT kcl.ac.uk>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Interpretation of constructors of type forall
- Date: Fri, 10 Dec 2010 15:31:29 +0000
- Organization: King's College, London
Hi,
In the definition of Trav below, how should one interpret Trav_S?
Inductive B : Set :=
Build_B : option B -> B.
Inductive Trav : B -> Prop :=
Trav_N : Trav (Build_B None) |
Trav_S : forall b : B, Trav (Build_B (Some b)) -> Trav b.
It strikes me as confusing to think of it as a constructor, because unlike Trav_N, it doesn't actually construct an object of type Trav <b>. It seems more appropriate to think of it as an object of type
forall b : B, Trav (Build_B (Some b)) -> Trav b
from which terms of type
Trav (Build_B (Some b')) -> Trav b'
can be produced by applying Trav_S to b'.
Thanks.
Regards,
Jeff.
- [Coq-Club] Interpretation of constructors of type forall, Jeffrey Terrell
Archive powered by MhonArc 2.6.16.