Re: [isabelle] Formalisations of infinite streams

On 14/06/2012, at 12:36 AM, Andreas Lochbihler wrote:

> 3. Peter Gammie recently defined coinductive streams as a codatatype which I have now added to Coinductive in the development AFP. Support for operations on streams is still quite limited.

Just to clarify: I found myself in need of a plausible coinductive stream type and adapted the LList formulation in the Coinductive development in the AFP.

Concretely I could have gotten away with nat => 'a, but hoped the coinductive formulation would be more convincing to people versed in type theory.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.