Stream: Beginner Questions

Topic: Order of arguments in mixfix

view this post on Zulip Adrián Doña Mateo (Jul 15 2022 at 10:05):

I've defined the following locale:

locale pre_strict_infinity_category =
  globular_set X s t for X :: "nat ⇒ 'a set" and s and t +
  fixes comp :: "nat ⇒ nat ⇒ 'a ⇒ 'a ⇒ 'a"
    and id :: "nat ⇒ 'a ⇒ 'a"

I would like to have custom notation for comp in the following fashion: g m∘n f = comp m n g f. I've had a look at Section 8.2 in the Isabelle/Isar reference manual, but I'm not familiar with context-free priority grammars. I believe the main issue is with changing the order in which the arguments appear. Could someone help me with this?

Last updated: Dec 21 2024 at 16:20 UTC