CODEWITHSUNDEEP
isabelle
Mike Shulman
Mike Shulman

Reputation: 167

How can I instantiate a typeclass at =>?

I am trying to use Isabelle/Pure as a logical framework to implement a proof assistant for a new logic (so Isabelle/HOL is irrelevant except as motivation).

Is there a way to define a typeclass instantiation for the function type =>, something like

instantiation "=>" :: (foo,foo)foo

so that whenever A and B are instantiations of foo then so will A => B automatically be? The above syntax isn't accepted; it seems that I need a name for the function-type constructor (not just a notation), but if such a name exists I don't know what it is or where to find it.

I am new to Isabelle, so please do tell me if what I am trying to do is the Wrong Thing for some reason.

Upvotes: 0

Views: 251

Answers (1)

René Thiemann
René Thiemann

Reputation: 1271

Yes, you can define a class instantiation for functions. It is no problem if you use the name of the type-constructor for functions fun, and not the infix operator =>.

For instance:

class foo = 
  fixes bar :: 'a

instantiation "fun" :: (foo,foo) foo
begin
definition "(bar :: 'a ⇒ 'b) = (λ x. bar)" 
instance ..
end

Two remarks:

  • the fun is in double quotes, since it would otherwise clash with the outer keyword fun to define functions.
  • in this example, you could also write instantiation "fun" :: (type,foo) foo, since the definition of bar for functions does not depend on the bar constant of type 'a.

Upvotes: 1

Related Questions