2

I have made a type of mine an instance of monoid_add:

instantiation "marking_ext" :: (monoid_add) monoid_add  
begin
  definition
    marking_add_def:
    "M + N = 
    ...
end

I can now use the familiar + notation between values of type ('a :: monoid_add) marking_ext, e.g., write M + N. But I would rather use \<oplus>, writing M \<oplus> N.

Can I change the notation of the typeclass instance, yet stay within the built-in hierarchy of type-classes?

2

You can add additional notation for + on your type, e.g. by introducing an abbreviation:

abbreviation marking_add' :: "marking_ext ⇒ marking_ext ⇒ marking_ext" (infixl "⊕" 65)
  where "(⊕) ≡ (+)"

You can tweak the operator precedence as needed (65 is the one that the normal + has).

Note, however, that introducing additional notation can be problematic if it clashes with notation in other theories. If someone wants to use your development in the future together with some other libraries that also define a notation , there will be syntax clashes and those can make life a bit harder for that person. There's usually a way to get around it (especially for simple notation like this one), but still: I would usually正规365体育投注 suggest not to use unnecessary extra notation unless there is a real benefit. In this particular case, I don't really see what the benefit would be. But that's just my advice, feel free to ignore it, of course! :)

|improve this answer|||||
  • Thanks! I’m formalizing parts of our work on declarative process modeling, and there’s some value in following the notation of published results when possible, I think. – Søren Debois Mar 28 at 8:55
1

The above answer gives me what I practically need, however, the /literal/ answer to the question turns out to be that you can change notation for a type class globally using notation:

notation plus (infixl "⊕" 65)

You probably won't want to do that for plus正规365体育投注, because if you do, arithmetic takes on your new look:

term "(2 :: nat) + 3"

--> "2 ⊕ 3"
  :: "nat"
|improve this answer|||||

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.