[isabelle] Overloading in locales
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
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
class Foo =
fixes foo :: "'a => bool"
instantiation A :: Foo
fun foo :: "A => bool" where
"foo x = True"
instantiation B :: Foo
fun foo :: "B => bool" where
"foo x = False"
I believe the second instantiation duplicates the declaration of foo.
Thanks for the help in advance.
This archive was generated by a fusion of
Pipermail (Mailman edition) and