Binding power

Stream: general

[Patrick Massot]

I still don't know enough binding power wizardry to do what I want. Say I have a binary operation #. How can I define it so that f a # b is parsed as f (a # b)? I tried putting random numbers where I expect Lean to expect binding powers, but failed.

[Patrick Massot]

Of course f is meant to be a function

[Kenny Lau]

is there any such operation in Lean?

[Kenny Lau]

iirc not even * has that priority

[Patrick Massot]

There are a lot of such operations in maths

[Johan Commelin]

They probably want us to use $...

[Patrick Massot]

I understand that, and actually I've get used to $ and use it a lot now. But the context for this question forbids this trick (we want one file from the perfectoid project to be readable by mathematicians who never saw any proof assistant or functional programming language)

[Kenny Lau]

I'm just pointing out that nothing overrides function application iirc

[Rob Lewis]

You just need to set the binding precedence high enough. But this isn't intended for mathlib, right? This goes against the normal notation customs and I think it would be very confusing.

infix `#`:10000 := has_add.add
def f : ℕ → bool := λ x, x < 5
#eval f 2 # 3

[Mario Carneiro]

Application is at precedence level 1024

[Mario Carneiro]

also known confusingly as max

[Mario Carneiro]

many unary prefix and postfix notations are at precedence "max_plus" which is max + 10

[Patrick Massot]

I tried with notation instead of infix, I guess this explains I couldn't do it

[Patrick Massot]

but with infix I get weird type class search issues

[Patrick Massot]

Lean doesn't seem to resolve instances when I use my notation (this has nothing to do with the precedence thing)

[Mario Carneiro]

does using local notation/infix help?

[Patrick Massot]

Do I need to define a class has_?

[Patrick Massot]

I'll try the local thing

[Patrick Massot]

it changes nothing

[Mario Carneiro]

details

[Patrick Massot]

notation R `∕` x := ideal.quotient (ideal.span ({x} : set R)) works fine but does not take precedence over function application. infix `∕`:max_plus := λ R x, (ideal.quotient (ideal.span ({x} : set R))) fails to find comm_ring R which is obvious

[Patrick Massot]

Note that this is not a regular / but unicode division sign

[Rob Lewis]

Does it work if you do def idq := λ R x, (ideal.quotient (ideal.span ({x} : set R))) and then infix `∕`:max_plus := idq?

[Rob Lewis]

With whatever type class instances you need in idq.

[Rob Lewis]

Make idq reducible if necessary.