Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 19 2022 at 08:02):

From: John Munroe <munddr@gmail.com>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 08:02):

From: Brian Huffman <huffman@in.tum.de>
Yes, it can, but you need to provide a definition for bar first.

Last updated: Apr 25 2024 at 20:15 UTC