no macro or `[quot_precheck]` instance for syntax kind

Stream: general

[Kevin Buzzard]

What does all this twaddle mean? This is from #4668

local notation x "𝖣" y => (KaehlerDifferential.kerTotal R S).mkQ (single y x) -- error
/-
no macro or `[quot_precheck]` instance for syntax kind 'Lean.Parser.Term.proj' found
  (KaehlerDifferential.kerTotal R S).mkQ
This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check.
-/

If I just go ahead and write set_option quotPrecheck false in above the definition then I get error expected token on z𝖣x a couple of lines later. However if I write set_option quotPrecheck false instead, then things look like they work. Thing is, I have no idea what I'm doing. Can anyone enlighten me? Note that R and S are indeed variables, and in Lean 3 the analogous line seemed to work fine.

[Kyle Miller]

If I were to guess, it's that R and S are variables? I don't think this is supported by the notation command. You could try using notation3 instead, but you might have to turn that dot notation into a normal function application to get a pretty printer (if you don't care about a pretty printer, the command will tell you an extra option to set)

[Kyle Miller]

Oh, maybe it's actually that it's that it's using dot notation, but still, I'm not sure notation supports variables so even if you switch it to using a function application it might give you another error

[Kevin Buzzard]

Yes R and S are variables, and this was Ok in Lean 3 for local notation.

[Yury G. Kudryashov]

Last time I had a similar problem, it was solved by using local macro instead of local notation.

[Yury G. Kudryashov]

See file#MeasureTheory/Integral/DivergenceTheorem

[Yury G. Kudryashov]

No, this file doesn't use local variables.

[Kevin Buzzard]

I don't know the syntax for local macro so am unable to check if this helps. local notation3 prompts me to write local notation3 (prettyPrint := false) which works but for some reason won't prettyprint...

[Matthew Ballard]

local macro x:term "𝖣" y:term : term => `((KaehlerDifferential.kerTotal R S).mkQ (single $y $x))

seems to work

[Mac Malone]

Kevin Buzzard said:

If I just go ahead and write set_option quotPrecheck false in above the definition then I get error expected token on z𝖣x a couple of lines later. However if I write set_option quotPrecheck false instead, then things look like they work.

The error itself is stating that the projection syntax (i.e., .mkQ) is not supported by the quotation prechecker, which is true. The notation command prechecks its definition, thus you get this error. To avoid this, you need to turn quotation prechecking off as you did with set_option quotPrecheck false.

However, the problem with set_option quotPrecheck false in <cmd> is that the in <cmd> syntax creates an anonymous section to wrap cmd in. Since local declarations are local only to their surrounding section, the definition immediately disappears once you leave the scope of the in. To get around this, you can just surround the definition with set_option. For example:

set_option quotPrecheck false
local notation x "𝖣" y => (KaehlerDifferential.kerTotal R S).mkQ (single y x)
set_option quotPrecheck true

Alternatively, as @Yury G. Kudryashov and @Matthew Ballard indicated, if you write this as a macro with a non-prechecked quotation (i.e., using `(...) instead of ``(...) ), you can also avoid the prechecking.

[Yaël Dillies]

Surely we should consider that a bug? That means we can't ever use set_option ... in local ....

[Mac Malone]

@Yaël Dillies Mario previously suggested opening an issue for it, but I do not think it ever manifested.

[Kyle Miller]

The notation command still won't be able to generate a pretty printer for this though, since it can't handle dot notation when it generates an unexpander, and I'm not sure it generates the correct unexpander when there are local variable-defined variables.

[Kyle Miller]

I pushed my first suggestion ("you could try using notation3 instead, but you might have to turn that dot notation into a normal function application"). You also need to make the coercion be explicit. These are some limitations with notation3 that could potentially be improved later.

Here's what it looks like:

local notation3 x "𝖣" y =>
  FunLike.coe (Submodule.mkQ (KaehlerDifferential.kerTotal R S)) (single y x)