CoList.agda

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

{- High-level intuition:

codata CoList (A : Set) : Set where
  nil : CoList A
  cons : A → CoList A → CoList A

append : ∀{A} → CoList A → CoList A → CoList A
append nil ys = ys
append (cons x xs) ys = cons x (append xs ys)

Co-pattern translation of code: -}

mutual
  data CoList (A : Set) : Set where
    nil : CoList A
    cons : CoCons A → CoList A
  
  record CoCons (A : Set) : Set where
    coinductive
    field
      hd : A
      tl : CoList A
open CoCons

mutual
  append : ∀{A} → CoList A → CoList A → CoList A
  append nil ys = ys
  append (cons xs) ys = cons (appendCons xs ys)
  
  appendCons : ∀{A} → CoCons A → CoList A → CoCons A
  hd (appendCons xs ys) = hd xs
  tl (appendCons xs ys) = append (tl xs) ys