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
> 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.