Infix functions

Stream: lean4

[J. O.]

When defining infix functions, is it nessacery for me to define the precedence? How can i figure out which precedence mine should have?

infixl:65   " + " => HAdd.hAdd  -- left-associative
infix:50    " = " => Eq         -- non-associative
infixr:80   " ^ " => HPow.hPow  -- right-associative
prefix:100  "-"   => Neg.neg
postfix:max "⁻¹"  => Inv.inv

[Mario Carneiro]

Yes, you should always define the precedence. I think the syntax allows you to omit it and it will do some default thing but I wouldn't trust it. I mean it's fine if you never "test" it, if you always put in enough parentheses to make it not matter, but if you ever have a precedence issue when using the notation then you should certainly put a precedence.

[Mario Carneiro]

As for how to determine the number, that's a bit hard because it's essentially a global problem: you should look at the precedences of all the other operations and for each other operation, decide how you want your operator to bind compared to that one, which will put inequality constraints on the numbers. After that it's arbitrary.

[Mario Carneiro]

For example, if you wanted to define x // y and the definitions you referenced are the only ones that are relevant, you should ask yourself:

• What should a // y + x mean?
  • If (a // y) + x, then p >= 65
  • If a // (y + x), then p <= 65
• What should a // y = x mean?
  • If (a // y) = x, then p >= 50
  • If a // (y = x), then p <= 50
• What should a // y ^ x mean?
  • If (a // y) ^ x, then p >= 80
  • If a // (y ^ x), then p <= 80
• What should -a // y mean?
  • If -(a // y), then p >= 100
  • If (-a) // y, then p <= 100
• What should a // y⁻¹ mean?
  • If (a // y)⁻¹, then p >= max
  • If a // (y⁻¹), then p <= max

Obviously some of these answers imply others, you can't have a value of p satisfying both p <= 50 and p >= 80 so keep that in mind. Also there is some wiggle room here if you choose p to be equal to one of the precedences listed; in that case the infixl / infixr / infix thing starts to matter. Usually you want to pick a value different from existing ones except in special cases like + and - where we don't want either one to "beat" the other: a + b - c means (a + b) - c but a - b + c means (a - b) + c.

[J. O.]

Thanks