[Agda] What is coinduction?

David Leduc david.leduc6 at googlemail.com
Tue Oct 5 02:43:59 CEST 2010


> 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


More information about the Agda mailing list