coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER C�dric <Cedric.Auger AT lri.fr>
- To: Satrajit Roy <satrajit.roy AT gmail.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Fwd: Forward reference
- Date: Wed, 12 Nov 2008 11:24:42 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Satrajit Roy a écrit :
> Hi guys,
>
> With reference to the following example, is there a way to forward
> reference Record y and use it in a function defined in Record x. For
> example, as an argument to createX or x''.
>
> Thanks again.
I am not sure to understand your question, do you want a mutually
recursive definition of Record?
It is sadly not yet possible for inductive, and for co-inductive
(http://coq.inria.fr/V8.2beta/CHANGES),
I don't know, but (exepted for extraction purpouses) you can "emulate"
Records as they just are
syntactical sugar.
For example,
>
> CoInductive A : Set :=
> | cons : A -> B -> A
> with B : Set :=
> | cons2 : A -> B -> B
> .
> Notation "'{' 'A_field' '=' x ';' 'B_field' '=' y '}'" := (cons x y).
> Notation "'{' 'A_field2' '=' x ';' 'B_field2' '=' y '}'" := (cons2 x y).
>
> Definition A_field A := match A with cons x _ => x end.
> Definition B_field A := match A with cons _ x => x end.
> Definition A_field2 B := match B with cons2 x _ => x end.
> Definition B_field2 B := match B with cons2 _ x => x end.
> Notation "A '.(A_field)'" := (A_field A) (at level 100).
> Notation "A '.(B_field)'" := (B_field A) (at level 100).
> Notation "B '.(A_field2)'" := (A_field2 B) (at level 100).
> Notation "B '.(B_field2)'" := (B_field2 B) (at level 100).
stands for:
Record A : Set :=
cons {A_field : A; B_field : B}
with B : Set :=
cons2 {A_field2 : A; B_field2 : B}.
(you even have better syntax as you can write {A_field = a; B_field = b}
instead of cons a b)
But send a more precise mail if I misunderstood you.
> ---------- Forwarded message ----------
> From: *Satrajit Roy*
>Â <satrajit.roy AT gmail.com
>Â <mailto:satrajit.roy AT gmail.com>>
> Date: Tue, Nov 11, 2008 at 11:01 AM
> Subject: Re: Lists & Strings
> To:
>Â coq-club AT pauillac.inria.fr
>
>Â <mailto:coq-club AT pauillac.inria.fr>
>
>
> Hi guys,
>
> How do I resolve the following:
>
> Require Export List.
> Require Export String.
>
> Module X.
>
> Record x: Set := createX {
> x': string;
> x'' : bool
> }.
>
> Record y: Set := createY {
> y': string;
> y'': list x;
>
> y''': bool :=
> match (length y') return bool with
> | 0 => false
> | _ => true
> end;
>
> y'''' : bool :=
> match (length y'') return bool with
> | 0 => false
> | _ => true
> end
> }.
>
> End X.
>
> which results in:
>
> Error:
> In environment
> y' : string
> y'' : list x
> y''' := (match length y'' with
> | 0 => false
> | S _ => true
> end:bool) : bool
> The term "y''" has type "list x" while it is expected to have type
> "string"
>
> Thanks , as always, for your time and effort.
>
- [Coq-Club] Fwd: Forward reference, Satrajit Roy
- Re: [Coq-Club] Fwd: Forward reference, AUGER Cédric
- Re: [Coq-Club] Fwd: Forward reference,
Satrajit Roy
- Re: [Coq-Club] Fwd: Forward reference, AUGER Cédric
- Re: [Coq-Club] Fwd: Forward reference,
Satrajit Roy
- Re: [Coq-Club] Fwd: Forward reference, AUGER Cédric
Archive powered by MhonArc 2.6.16.