The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

Consider the following.

Parameter set : list nat.

CoInductive trace : LList nat -> Prop :=

  | empty : trace LNil

  | step  : forall l, exists n, In n set -> 

            trace l ->

            trace  (LCons n l).

The above does not typecheck, as the scope of the existential quantification goes up to the conclusion. Of course, if I put parentheses then variable n is no longer in scope...

I want  to model the fact that I can pick any element from set, and include the picked element in the predicate conclusion..

How would you go about this? :)

Cheers.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.