Errors after update

Stream: lean4

[Dan Velleman]

I just updated a project to leanprover/lean4:nightly-2023-02-10 and I'm getting errors I don't understand. On this definition:

open Lean

def mkExists (l : Level) (x : Name) (bi : BinderInfo) (t b : Expr) : Expr :=
  mkApp2 (mkConst ``Exists [l]) t (mkLambda x bi t b)

I get an error on mkApp2. The error is unknown identifier 'mkApp2'. If I add import Mathlib (which I wouldn't think would have anything to do with this), then the error on mkApp2 goes away, but I get an error on the l of mkConst ``Exists [l]. The error is expected '⁻¹]'.

Anyone know what I'm doing wrong?

[Dan Velleman]

This worked on a nightly from about a week earlier.

[Dan Velleman]

OK, I understand the first error. I was trying to make a MWE by pulling this definition out of a larger file, and I forgot to include a required import. But I still don't understand the second error, which is the error I started getting in the larger file when I updated from nightlly-2023-02-03 to nightly-2023-02-10.

[Reid Barton]

Presumably due to this somehow:

Mathlib/RingTheory/OreLocalization/Basic.lean:notation:1075 R "[" S "⁻¹]" => OreLocalization R S

[Reid Barton]

You were trying to invert the ring Exists at l, right?

[Dan Velleman]

Yes, that must be it. So how do I write a list with one entry now without Lean expecting a superscript -1?

[Ruben Van de Velde]

Maybe [(x\inv)]

[Reid Barton]

I guess for now you can not import all of mathlib

[Dan Velleman]

Do I have to write l :: [] now?

[Reid Barton]

That also works

[Reid Barton]

(I hope)

[Dan Velleman]

What is the purpose of the 1075 in the notation declaration? Does that set this notation to have a very high precedence? Is that the reason Lean is preferring this interpretation over the List interpretation?

[Kevin Buzzard]

The binding power of 1075 is even bigger than function application (or at least it was in Lean 3)

[Sebastian Ullrich]

That mathlib notation should probably use noWs (for which it needs to become a macro)

[François G. Dorais]

Perhaps it should also be scoped? Ring localization is not that widespread.