Playing with co-patterns in Agda

gistfile1.agda

{-# OPTIONS --copatterns #-}
module Test where

open import Data.Nat
open import Data.Bool
open import Data.Vec hiding (map; head; tail; take)

record Functor (F : Set → Set) : Set₁ where
  field
    map : ∀ {A B} → (A → B) → F A → F B
open Functor ⦃...⦄ public

record Stream (A : Set) : Set where
  coinductive
  constructor _∷_
  field  
    head : A
    tail : Stream A
infixr 40 _∷_
open Stream public

instance
  streamFunctor : Functor Stream
  streamFunctor = record { map = stream-map }
    where
      stream-map : ∀ {A B} → (A → B) → Stream A → Stream B
      head (stream-map f xs) = f (head xs)
      tail (stream-map f xs) = stream-map f (tail xs)

trues : Stream Bool
head trues = true
tail trues = trues

take : ∀ {A} → (n : ℕ) → Stream A → Vec A n
take zero    xs = []
take (suc n) xs = head xs ∷ take n (tail xs)

test-map : Vec Bool 10
test-map = take 10 (map not trues)