[isabelle] primcorec on enat



Dear all,

 

I?m currently trying to develop an Isabelle/HOL Theory using the new
?codatatype? package.

 

I have constructed a simple codatatype similar to a lazy list and wanted to
implement a primitive corecursive function which returns the length of this
list as an enat (extended natural number from the
Coinductive/Coinductive_Nat package).

 

My problem is now that I get an error message ?enat is not a codatatype?.
Thus, it cannot be used as a return type for corecursive functions.

My question is now whether someone knows about an implementation of extended
natural numbers as codatatype so that it can be used as return value for
corecursive functions?

 

 

Many thanks,

 

Best,

 

Diego

 

--

Diego Marmsoler

Technische Universität München

Fakultät für Informatik

Lehrstuhl für Software & Systems Engineering

Zimmer MI 00.11.057

Boltzmannstr. 3

85748 Garching bei München

Tel. +49 (0)89 289-17384 

Fax. +49 (0)89 289-17307

 <mailto:diego.marmsoler at tum.de> diego.marmsoler at tum.de

 <http://www4.in.tum.de/~marmsole/> http://www4.in.tum.de/~marmsole/

 

 

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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