The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I'm wondering if someone can summarize the *theoretical* differences between the two definitions:

CoInductive trace (state : Type) : Type :=

| Cons : state -> trace state -> trace state.

and

Definition trace (state : Type) : Type := nat -> state.

To reason about the first I use co-induction and I do not need functional extensionality. The second definition requires functional extensionality in most cases. Other than this, are there reasons to prefer one over the other from a theoretical point of view?

Thanks.

--

gregory malecha