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



On Mon, Jul 30, 2012 at 11:47 PM, John Munroe <munddr at gmail.com> wrote:
> 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?

Yes, it can, but you need to provide a definition for bar first.

- Brian





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