Re: [isabelle] Type as argument



If you employ type classes, you could simulate the behaviour of functions taking types as arguments in a restricted way.
For most applications, the type classes usually suffice.


Lukas


On 05/13/2011 05:58 PM, Tobias Nipkow wrote:
Types live on the meta-level and are not terms. Hence they cannot be arguments of functions either. Sorry.

Tobias

Am 13/05/2011 17:16, schrieb Steve W:
Hi,

I have a quick question: does anyone know how to define a function taking a type as an argument? Say, a function f taking the type "nat" as an argument.

Thank you
Steve







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