# Re: [isabelle] Type as argument

Thanks all. One more question: what is the "itself" keyword for in "'a
itself"?
Thanks
Steve
2011/5/13 René Thiemann <rene.thiemann at uibk.ac.at>
> > Thanks. If I change f to a binary function:
> >
> > class foo =
> > fixes f :: "int => 'a itself => int"
> >
> > and with the following instantiation:
> >
> > instantiation nat :: foo
> > begin
> > definition "f 0 (t::nat itself) = 0"
> > instance ..
> > end
> >
> > I get an error on "0::int". It works if 0 is replaced by a free variable
> > though. Why's that?
>
> Because "definition" cannot be used with pattern matching on left-hand
> sides.
> Usually, one can use "fun" instead. However, even with "fun" you cannot
> do pattern matching on "int" instead of "nat".
>
> However, you might write "f x (t:: nat itself) = (if x = (0 :: int) then 0
> else ...)"
>
> René
> --
> René Thiemann mailto:rene.thiemann at uibk.ac.at
> Computational Logic Group
> http://cl-informatik.uibk.ac.at/~thiemann/
> Institute of Computer Science phone: +43 512 507-6434
> University of Innsbruck
>
>

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