The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hello Vladimir,

does this serve your purpose?

Variable A : Type.
Variable a : A.

CoInductive Stream (P : A -> Prop) : Type :=
  cons : forall
          (head : { x : A | P x } -> A)
          (tail : Stream (fun x => forall (p : P x),
                            head (exist (fun x => P x) x p) = a)),
         Stream P.

Definition VS := Stream (fun x => True).

Cheers,
Andreas

On 27.06.11 2:30 AM, Vladimir Voevodsky wrote:
> Is there a way to define in Coq the type which can be informally
> described as follows:
>
> 1. Given parameters A : Type , a : A .
>
> 2. I want to define the type of (infinite) sequences f_0 ,..., f_n,
> .... where
>
> 2a. f_0 : A ->  A .
>
> 2b. f_{S n} : {| x : A ; f_n x = a |} ->  A .
>
> Is there a way to define the type of such sequences ?

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/