Могу ли я изменить обозначения во встроенном классе Изабель типа

Question

Я сделал свой тип экземпляром monoid_add:

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

Теперь я могу использовать знакомую нотацию + между значениями типа ('a :: monoid_add) marking_ext, например, написать M + N , Но я бы предпочел использовать \<oplus>, написав M \<oplus> N.

Могу ли я изменить нотацию экземпляра класса типов, оставаясь при этом во встроенной иерархии классов типов?

Answer 1

Вы можете добавить дополнительные обозначения для + для вашего типа, например, введя аббревиатуру:

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

При необходимости вы можете настроить приоритет оператора (65 - это то, что обычно +). has).

Обратите внимание, однако, что введение дополнительных обозначений может быть проблематичным c, если оно вступает в противоречие с обозначениями в других теориях. Если кто-то захочет использовать вашу разработку в будущем вместе с некоторыми другими библиотеками, которые также определяют нотацию ⊕, возникнут синтаксические конфликты, и это может сделать жизнь этого человека немного сложнее. Обычно есть способ обойти это (особенно для простых обозначений, подобных этому), но все же: я бы обычно предложил бы не использовать ненужные дополнительные обозначения, если нет реальной выгоды. В данном конкретном случае я не очень понимаю, какую пользу это принесет. Но это только мой совет, не стесняйтесь, конечно, игнорировать его! :)

Answer 2

Приведенный выше ответ дает мне то, что мне практически необходимо, однако / literal / ответ на вопрос оказывается таким, что вы можете изменить нотацию для класса типов глобально, используя notation:

notation plus (infixl "⊕" 65)

Вы, вероятно, не захотите делать это для plus, потому что если вы это сделаете, арифметика c приобретет ваш новый вид:

term "(2 :: nat) + 3"

--> "2 ⊕ 3"
  :: "nat"