Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.