Zulip Chat Archive

Stream: general

Topic: Precedence of function application


view this post on Zulip Joe Hendrix (Aug 07 2018 at 22:49):

Can notation bind tighter than function application? e.g. For an operator ^ make f x ^ y parse as f (x ^ y)?

view this post on Zulip Chris Hughes (Aug 07 2018 at 22:57):

I think not.

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 22:57):

I think that (a) function application has super-high binding power and (b) if you want to use notation which already exists in Lean (like ^) then, whilst you can define it to mean new things, you cannot change its default binding power, which is lower than the super-high binding power of functions. So at the very least you would have to use notation which is not already used in Lean, e.g. \clubsuit or some random thing like that.

view this post on Zulip Joe Hendrix (Aug 07 2018 at 23:12):

Yes, I meant "^" as a placeholder. It looks like I can, but it was a much higher binding power than I tested at first.

view this post on Zulip Joe Hendrix (Aug 07 2018 at 23:16):

This seemed to work, but if the precedence is any lower it doesn't.

set_option pp.all true

infix ` <> `:1025 := and
constant f : Prop → Prop
#check f true <> false

Anyways, thanks for suggesting the "super-high" binding power.

view this post on Zulip Mario Carneiro (Aug 08 2018 at 00:18):

Yes, you can. The binding power of application is max = 1024, which despite the name is not the maximum possible bonding power; you can see max+10 used in the core.lean file.

view this post on Zulip François G. Dorais (Aug 08 2018 at 00:28):

BTW: max_plus is useful, it evaluates to 1034 (aka max+10) and avoids silly incidents like max+11 (aka max_spinal_tap).


Last updated: May 08 2021 at 03:17 UTC