module Coind where

open import Coinduction
open import Data.Nat hiding(fold)
open import Data.Vec hiding(take;zipWith;tail)

data Coℕ : Set where
  zero : Coℕ
  suc  : ∞ Coℕ → Coℕ

inf : Coℕ
inf = suc ( ♯ inf )

data Stream (A : Set) : Set where
  _∷_ : (x : A) → (xs : ∞ (Stream A)) → Stream A
infixr 6  _∷_

take : {A : Set} → (n : ℕ) → Stream A → Vec A n
take zero xs = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)

zeros : Stream ℕ
zeros = zero ∷ ♯ zeros

test₁ : Stream ℕ
test₁ = 1 ∷ ♯ (2 ∷ ♯ (3 ∷ ♯ zeros))

zipWith : {A B C : Set} → (A → B → C) → Stream A → Stream B → Stream C
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ ♯ zipWith f (♭ xs) (♭ ys)

tail : {A : Set} → Stream A → Stream A
tail (x ∷ xs) = ♭ xs

{-# NON_TERMINATING #-}
fib : Stream ℕ
fib = 0 ∷ ♯ (1 ∷ ♯ (zipWith _+_ fib (tail fib)))