ROSCOQ.CoList

Set Implicit Arguments.

CoInductive CoList (A : Type) : Type :=
    cnil : CoList A | ccons : A → CoList A → CoList A.


Extraction Language Haskell.


Extract Inductive CoList ⇒ "([])" [ "[]" " (:)" ].

Extract Inductive list ⇒ "([])" [ "[]" " (:)" ].

Fixpoint initialSegment {A} (len : nat) (cl : CoList A) : list A :=
match len with
| 0 ⇒ nil
| S len' ⇒ match cl with
         | cnil _ ⇒ nil
         | ccons hd tl ⇒ cons hd (initialSegment len' tl)
         end
end.

Section Map.
  Variables A B : Type.
  Variable f : A → B.

CoFixpoint coMap (l:CoList A) : CoList B :=
    match l with
      | cnil _ ⇒ cnil B
      | ccons a t ⇒ ccons (f a) (coMap t)
    end.

End Map.