binding powers

Stream: general

[Kenny Lau]

What's the right way to declare a notation for a ^[b] c? what should the binding powers of ^[ and ] be?

[Simon Hudon]

] should have a maximal binding power ( :max ) and you should chose a binding power for ^[ comparable to the operators it will be used with. If it's to be used as ^, look at its binding power with #print notation ^

[Kenny Lau]

thanks

[Kenny Lau]

@Simon Hudon it still behaves differently from a ^ c

[Simon Hudon]

How so?

[Mario Carneiro]

shouldn't ] get minimum binding power?

[Kenny Lau]

M ⊗ N → M ⊗ N parses as (M ⊗ N) → (M ⊗ N) as intended, but I can't get M ⊗[R] N → M ⊗[R] N to be parsed the same

[Kenny Lau]

neither 0 nor max work

[Simon Hudon]

If you put brackets around one of the two sides of the expression, that should fix the problem and tell me where the problem is. Can you try bracketing only one side at a time and tell me where the problem is?

[Kenny Lau]

(M ⊗[R] N) → M ⊗[R] N parses as intended

[Simon Hudon]

Did you make the binding power of ] 0 or max?

[Kenny Lau]

both

[Kenny Lau]

the situation is same for both

[Mario Carneiro]

did you try making the bp the same as the open bracket?

[Kenny Lau]

M ⊗[R] N → M ⊗[R] N is parsed as M ⊗[R] (N → (M ⊗[R] N))

[Kenny Lau]

did you try making the bp the same as the open bracket?

it hangs

[Mario Carneiro]

also is the bp greater than 25 or less?

[Kenny Lau]

M ⊗[R] N → M ⊗[R] N is parsed as M ⊗[R] (N → (M ⊗[R] N)) for (⊗[=100 and ]=0) and (⊗[=100 and ]=max)

[Mario Carneiro]

this works:

constant tensor : Type → Type → Type → Type

notation M ` ⊗[`:30 R `] ` N:30 := tensor R M N

example {M R N : Type} :
  (M ⊗[R] M ⊗[R] N -> M ⊗[R] N) = (((M ⊗[R] M) ⊗[R] N) -> (M ⊗[R] N)) := rfl

[Kenny Lau]

interesting

[Kenny Lau]

I don't understand binding powers

[Kenny Lau]

how can N have a binding power

[Mario Carneiro]

me neither, I just put a bunch of stuff in there until it worked

[Mario Carneiro]

actually it makes more sense to give a variable a binding power than a constant

[Mario Carneiro]

when a variable has a bp it means that the expression there is parsed with that bp

[Mario Carneiro]

if it sees a constant with a lower bp than the one currently used in the parse, it acts as though a ) is inserted

[Patrick Massot]

I have a new binding power challenge!

notation `|`x`|` := abs x
variables (x : ℤ)
#check |x|  -- works
#check (|x|) -- fails!
#check ( |x| ) -- works!

[Patrick Massot]

The challenge is to fix the first line so that all lines work

[Patrick Massot]

It took me for ever to understand what was happening when I hit this in the wild

[Simon Hudon]

have you tried #print notation (| |)?

[Patrick Massot]

no notation

[Patrick Massot]

but I didn't try before, thanks!

[Patrick Massot]

Any other suggestion?

[Simon Hudon]

What about just #print notation (|?

[Sebastian Ullrich]

(| |) is ASCII syntax for the anonymous constructor

[Patrick Massot]

nooo!

[Patrick Massot]

Can I override that?

[Patrick Massot]

Can you remove ascii from Lean 4?

[Sebastian Ullrich]

Not in Lean 3

[Sebastian Ullrich]

You can do that yourself in Lean 4 :P

[Patrick Massot]

What about just #print notation (|?

no notation

[Patrick Massot]

Preventing (| from being used is really really sad

[Simon Hudon]

In general, I think scoping notations will be very useful in Lean 4

[Patrick Massot]

Kevin, what did you do with absolute values in your classes? Did you use a fancy |? Or were you lucky with parentheses?

[Kevin Buzzard]

No, I discovered exactly the same thing as you, tried to fix it, couldn't, so just started putting spaces after brackets.

[Kevin Buzzard]

I didn't know why it was failing though, so this thread has been helpful!