How to make a < b < c = a < b ∧ b < c shorthand notation?

Stream: new members

[aron]

This doesn't quite work, it gives an error unexpected token ':='; expected '<':

/-- The syntax for chained lt -/
notation a "<" b "<" c => a < b ∧ b < c
/-- The syntax for chained gt -/
notation a ">" b ">" c => a > b ∧ b > c
/-- The syntax for chained lte -/
notation a "≤" b "≤" c => a ≤ b ∧ b ≤ c
/-- The syntax for chained gte -/
notation a "≥" b "≥" c => a ≥ b ∧ b ≥ c


variable (a b c : Nat)
example : a < b < c := by sorry

What's the right or best way to support this kind of syntax?

[Robin Arnez]

You need to specify precedence:

/-- The syntax for chained lt -/
notation:50 a:51 " < " b:51 " < " c:51 => a < b ∧ b < c
/-- The syntax for chained gt -/
notation:50 a:51 " > " b:51 " > " c:51 => a > b ∧ b > c
/-- The syntax for chained le -/
notation:50 a:51 " ≤ " b:51 " ≤ " c:51 => a ≤ b ∧ b ≤ c
/-- The syntax for chained ge -/
notation:50 a:51 " ≥ " b:51 " ≥ " c:51 => a ≥ b ∧ b ≥ c

[aron]

thanks @Robin Arnez that seems to work! can you explain a little more about how this fixes it? where do the 50 and 51s come from?

[Robin Arnez]

50 is the precedence of <, =, > etc. and we just need to make sure the precedence of the arguments is higher to make sure you couldn't put an a < b < c as an argument (in the sense of (1 < 2 < 3) < 4 < 5 working without parentheses)