Re: [isabelle] Type as argument
> 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
> definition "f 0 (t::nat itself) = 0"
> instance ..
> 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é 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