Andreas Lochbihler 🌐 with contributions from Johannes Hölzl 📧

February 12, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This article collects formalisations of general-purpose coinductive data types and sets. Currently, it contains coinductive natural numbers, coinductive lists, i.e. lazy lists or streams, infinite streams, coinductive terminated lists, coinductive resumptions, a library of operations on coinductive lists, and a version of König's lemma as an application for coinductive lists.
The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.
BSD License


Theories of Coinductive