4.6 Coinductive types

The implementation contains also coinductive definitions, which are types inhabited by infinite objects.