[isabelle] Overloading in locales



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





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