parsing ⇑

Stream: mathlib4

[Scott Morrison]

@Gabriel Ebner, parsing ⇑ (from Mathlib/Coe.lean) is not working correctly: e.g. I have a ⇑e.toOrderEmbedding = e which is giving the error cannot coerce to function toOrderEmbedding e = RelIso.toRelEmbedding e. Changing this to (⇑e.toOrderEmbedding) = e works fine.

[Mario Carneiro]

that sounds like a precedence issue

[Mario Carneiro]

I would guess it needs a precedence in the range of 100

[Mario Carneiro]

It doesn't have a declared precedence, which I think means it is max on the left and 0 on the right, i.e. it consumes everything after it

[Mario Carneiro]

ah, actually it's leadPrec not maxPrec but it doesn't make much difference

[Scott Morrison]

How do I add the precedence?

[Mario Carneiro]

elab:leftPrec "⇑" x:term:rightPrec

[Mario Carneiro]

having the default (high) left prec seems fine but the right prec should be at least 70 so that it goes above the usual binary operators