[isabelle] Overloading a function: "Extra variables on rhs"



Hi,

I'm trying to overload two functions:

class C =
  fixes foo :: "'a => int"
  and bar :: "'a => int"

instantiation int :: C
begin
definition "foo (x::int) = bar (x::int) + 1"

Basically I'm trying to define foo(x) in terms of bar(x). Can it be
done in a type class?

Thanks

John





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