[problem_57.lean] Potential ambiguity in expression on L32

[kmd710]

Hi,

I was looking at this line:

clever/src/lean4/human_eval/problem_57.lean

Line 32 in 3675fb7

result ↔ ¬non_ordered;

I may be mistaken, but the expression 1 < numbers.length → result ↔ ¬non_ordered seems ambiguous regarding operator precedence without parentheses.

Could you clarify this by adding parentheses? For example:
(1 < numbers.length) → (result ↔ ¬non_ordered)

As a side note, when I tried adding the parentheses like this, I was able to get a solution in lean with unlimited vericoding (i.e., in an Agent mode without time limits).

Thanks!

[amit9oct]

Hi @kmd710 ,
Thanks for letting me know. Let me take another look at it, and I will get back to you.

[amit9oct]

Sorry for the delay, we can add this precedence. It should not be a problem.

[amit9oct]

@kmd710 merged with #66 . Thank you for opening the issue.