The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT inria.fr>]

Hi,

The definition in theory/LISTS/Streams.v comes from a Coq development
I did some time ago, where I would like the "witness" of P to be the
first possible one in the sequence. I agree that the following
non-deterministic version of the predicate is closer to the intended
meaning of "there exists some element of the sequence that verifies
P":

Inductive   Exists :  Stream -> Prop :=
   Here    : (x:Stream)(P x) ->(Exists x) |
   Further : (x:Stream)(Exists (tl x))->(Exists x).


Sincerely,
Eduardo Gimenez.