ext.v

Require Extraction.

Inductive list (A : Type) : Type :=
 | nil : list A
 | cons : A -> list A -> list A.

CoInductive Stream (A : Type) :=
  Cons : A -> Stream A -> Stream A.

Extraction Language Haskell.
Extraction list.
Extraction Stream.
(* ->
data List a =
   Nil
 | Cons a (List a)


data Stream a =
   Cons a (Stream a)
 *)

Extraction Language OCaml.
Extraction list.
Extraction Stream.
(* ->
type 'a list =
| Nil
| Cons of 'a * 'a list
type 'a stream = 'a __stream Lazy.t
and 'a __stream =
| Cons of 'a * 'a stream
 *)