Universe binder syntax

Stream: general

[Eric Wieser]

I was surprised to find that {u} binder syntax works for some commands but not others:

-- ok
def {w} foo1 {Q : Type w} := Q
abbreviation {w} foo2 {Q : Type w} := Q
lemma {w} foo3 {Q : Type w} : Type w := Q
-- fail
instance {w} foo4 {Q : Type w} : Type w := Q

Is this deliberate?

[Gabriel Ebner]

Eric Wieser said:

Is this deliberate?

No.

[Eric Wieser]

Edited, I screwed up on the lemma one.

[Eric Wieser]

I guess the problem with instance is that you then don't know how to parse

instance {w} {Q : Type w} : Type w := Q

[Eric Wieser]

I'm asking these because the new syntax highlighter gets highlighting slightly wrong on instance {R : Type}

[Eric Wieser]

leanprover/vscode-lean#269

[Eric Rodriguez]

@Eric Wieser , these get messed up by }} brackets:

image.png

[Eric Wieser]

Can you paste a mwe so that I can debug?

[Eric Wieser]

Ah, it's an easy fix - the binder name regex seems to think ⦄ is allowed as part of an unquoted name

[Eric Wieser]

That is, these patterns need to include that character in their forbidden-symbol list:

https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json#L225-L236

[Eric Rodriguez]

you're fast - didn't even finish writing the MWE in time!

[Bhavik Mehta]

Is this fix in the process of being PR'd? I'm hitting this a lot today :(

[Eric Wieser]

Is it the same bug?

[Eric Wieser]

I haven't gotten around to Pring it, but it's a 4-charcter fix

[Bhavik Mehta]

It seems like it, yeah, everything after a }} looks completely broken in my VSCode

[Eric Wieser]

Will PR it now

[Bhavik Mehta]

Thanks!

[Eric Wieser]

https://github.com/leanprover/vscode-lean/pull/270