Re: [isabelle] Type as argument

Types live on the meta-level and are not terms. Hence they cannot be arguments of functions either. Sorry.


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

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

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