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