Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Interpretation of constructors of type forall

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Interpretation of constructors of type forall


chronological Thread 
  • 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.



Archive powered by MhonArc 2.6.16.

Top of Page