Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Overloading in locales

Email Gateway (Aug 18 2022 at 18:14):

From: John Munroe <munddr@gmail.com>
Hi,

Thanks for the pointer to overloading. Can the class declaring the
class operation or the instantiation of the class be constructed
within a locale? i.e., using the example in the tutorial:

class plus =
fixes plus :: "'a => 'a => 'a"

instantiation nat :: plus
begin
primrec plus_nat :: "nat => nat => nat" where ...

Can all or part of the overloading happen inside a locale rather than
at the top level, e.g., can the instantiation of plus be created
inside a locale?

Also, if I were to overload a function 'foo' that returns true if the
input is of type A and false if it's of type B, then is the following
correct?

class Foo =
fixes foo :: "'a => bool"

typedecl A
typedecl B

instantiation A :: Foo
begin
fun foo :: "A => bool" where
"foo x = True"
instance ..
end

instantiation B :: Foo
begin
fun foo :: "B => bool" where
"foo x = False"
instance ..
end

I believe the second instantiation duplicates the declaration of foo.

Thanks for the help in advance.

John

Email Gateway (Aug 18 2022 at 18:15):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,

Thanks for the pointer to overloading. Can the class declaring the
class operation or the instantiation of the class be constructed
within a locale?

Can all or part of the overloading happen inside a locale rather than
at the top level, e.g., can the instantiation of plus be created
inside a locale?

Class instantiations are always global, since there is no concept of
»local sort algebra« or such in Isabelle.

Also, if I were to overload a function 'foo' that returns true if the
input is of type A and false if it's of type B, then is the following
correct?

Rule of thumb: Try out and report if you get into problems ;-)

Regards,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC