As an example, imagine we want to represent 1/3, (that is 0.33333 recuring).

We could have a recursive data structure where we can continue adding '3's onto the end and read them out when required.

Perhaps we might represent an infinite sequence of threes like this:

data Threes = Threes

but it could never be constructed

### Data

||| Natural numbers: unbounded, unsigned integers which can be pattern ||| matched. data Nat = ||| Zero Z | ||| Successor S Nat

data List : (elem : Type) -> Type where ||| Empty list Nil : List elem ||| A non-empty list, consisting of a head element and the rest of ||| the list. (::) : (x : elem) -> (xs : List elem) -> List elem

### CoData

data Stream : Type -> Type where (::) : (e : a) -> Inf (Stream a) -> Stream a ||| The first element of an infinite stream head : Stream a -> a head (x::xs) = x ||| All but the first element tail : Stream a -> Stream a tail (x::xs) = xs