parentheses weirdness

Stream: lean4

[Arthur Paulino]

@Daniel Rogozin and I found a strange behavior here. For some reason, removing the parentheses around 2^(m - iMax - 1) makes #eval tonelli 10 13 loop forever. Has anyone seen this before? Thanks!

[Arthur Paulino]

Ah, nevermind. I see what's happening. Without the parentheses, that line is equivalent to let b := (powMod p c 2)^(m - iMax - 1)

[Arthur Paulino]

In Python and Javascript, 2 + 3**3 equals 29. But in Lean 4, 2 + 3^3 equals 125. Is this the precedence we want? Looks a bit confusing to me :thinking:

[Patrick Massot]

Very confusing indeed.

[James Gallicchio]

I think funapp precedence should still be higher than ^, so I'd expect the parentheses to still be needed in the tonelli code. But it's weird that the pow precedence is lower than add, that seems like a bug

[Arthur Paulino]

James Gallicchio said:

I think funapp precedence should still be higher than ^

I disagree with this even. The fact that this breaks is just weird:

def add3 : Nat → Nat → Nat → Nat := fun a b c => a + b + c
#eval add3 2 3^3 4

But this is subjective

[James Gallicchio]

Oh wait, with just Std imported, 2 + 3^3 is 29... does your code redefine the add notation?

[James Gallicchio]

Arthur Paulino said:

But this is subjective

bleh, it is subjective, but most FP langs have a very strict rule that funapp always has highest precedence. I think Lean gives funapp maximum precedence too.

[Arthur Paulino]

Okay nevermind. I don't know what I did. #eval 2 + 3^3 now returns 29 :dizzy:

[Arthur Paulino]

James Gallicchio said:

Oh wait, with just Std imported, 2 + 3^3 is 29... does your code redefine the add notation?

Thanks for double checking :pray:

[Yaël Dillies]

docs#has_compl.compl has higher precedence than function application and I must say it is quite a practical exception

[Reid Barton]

Same for opposite https://github.com/leanprover-community/mathlib/blob/160ef3e338a2a4f21a280e4c152d4016156e516d/src/data/opposite.lean#L47-L49

[Reid Barton]

These are postfix notations though, I am less sure about ^.