Zulip Chat Archive

Stream: general

Topic: binding powers


Kenny Lau (Jan 26 2019 at 03:09):

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

Simon Hudon (Jan 26 2019 at 03:24):

] 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 (Jan 26 2019 at 03:36):

thanks

Kenny Lau (Jan 26 2019 at 03:38):

@Simon Hudon it still behaves differently from a ^ c

Simon Hudon (Jan 26 2019 at 03:38):

How so?

Mario Carneiro (Jan 26 2019 at 03:38):

shouldn't ] get minimum binding power?

Kenny Lau (Jan 26 2019 at 03:40):

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 (Jan 26 2019 at 03:40):

neither 0 nor max work

Simon Hudon (Jan 26 2019 at 03:42):

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 (Jan 26 2019 at 03:43):

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

Simon Hudon (Jan 26 2019 at 03:44):

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

Kenny Lau (Jan 26 2019 at 03:44):

both

Kenny Lau (Jan 26 2019 at 03:44):

the situation is same for both

Mario Carneiro (Jan 26 2019 at 03:44):

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

Kenny Lau (Jan 26 2019 at 03:44):

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

Kenny Lau (Jan 26 2019 at 03:45):

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

it hangs

Mario Carneiro (Jan 26 2019 at 03:45):

also is the bp greater than 25 or less?

Kenny Lau (Jan 26 2019 at 03:46):

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 (Jan 26 2019 at 03:54):

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 (Jan 26 2019 at 03:54):

interesting

Kenny Lau (Jan 26 2019 at 03:54):

I don't understand binding powers

Kenny Lau (Jan 26 2019 at 03:55):

how can N have a binding power

Mario Carneiro (Jan 26 2019 at 03:55):

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

Mario Carneiro (Jan 26 2019 at 03:55):

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

Mario Carneiro (Jan 26 2019 at 03:55):

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

Mario Carneiro (Jan 26 2019 at 03:56):

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 (Jan 26 2019 at 22:13):

I have a new binding power challenge!

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

Patrick Massot (Jan 26 2019 at 22:13):

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

Patrick Massot (Jan 26 2019 at 22:14):

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

Simon Hudon (Jan 26 2019 at 22:15):

have you tried #print notation (| |)?

Patrick Massot (Jan 26 2019 at 22:15):

no notation

Patrick Massot (Jan 26 2019 at 22:16):

but I didn't try before, thanks!

Patrick Massot (Jan 26 2019 at 22:19):

Any other suggestion?

Simon Hudon (Jan 26 2019 at 22:22):

What about just #print notation (|?

Sebastian Ullrich (Jan 26 2019 at 22:23):

(| |) is ASCII syntax for the anonymous constructor

Patrick Massot (Jan 26 2019 at 22:23):

nooo!

Patrick Massot (Jan 26 2019 at 22:23):

Can I override that?

Patrick Massot (Jan 26 2019 at 22:23):

Can you remove ascii from Lean 4?

Sebastian Ullrich (Jan 26 2019 at 22:23):

Not in Lean 3

Sebastian Ullrich (Jan 26 2019 at 22:24):

You can do that yourself in Lean 4 :P

Patrick Massot (Jan 26 2019 at 22:25):

What about just #print notation (|?

no notation

Patrick Massot (Jan 26 2019 at 22:26):

Preventing (| from being used is really really sad

Simon Hudon (Jan 26 2019 at 22:27):

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

Patrick Massot (Jan 26 2019 at 22:38):

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

Kevin Buzzard (Jan 26 2019 at 22:42):

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

Kevin Buzzard (Jan 26 2019 at 22:43):

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


Last updated: Dec 20 2023 at 11:08 UTC