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