> Would someone be kind enough to give me a brief explanation about what the > point of Coinduction/Codata is? This is to define the type of infinite objects such as the infinite stream of 0: inf0 : stream Nat inf = 0 :: inf