Unclear Error Message

Stream: general

[Asei Inoue]

When running the following code, it produces the error "unknown identifier 'Unexpander'".
However, the actual cause of the error is the in at the end of the set_option line.
If you remove the in, the error disappears.
This error message is hard to understand, in my opinion.

set_option linter.unusedVariables false in

open Lean PrettyPrinter

def unexpander : Unexpander := fun stx =>
  match stx with
  | _ => throw ()

[Aaron Liu]

It fails to parse but doesn't throw an error???

[Damiano Testa]

Is this caused by the fact that the in makes the open finish its scope as soon as it's over?

[Damiano Testa]

So then Unexpanded is unknown, since it is missing some namespace?

[Damiano Testa]

A good mental model for in is that it wraps the following command inside a section/end pair, so the open command is only opening the namespaces in a very very very narrow margin.

[Aaron Liu]

It looks like

set_option linter.unusedVariables false in

open Lean PrettyPrinter

is one command

[Damiano Testa]

I agree, and the command is roughly equivalent to section (...) end.

[Robin Arnez]

Damiano Testa schrieb:

I agree, and the command is roughly equivalent to section (...) end.

Not just roughly:

@[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
  | `($cmd₁ in%$tk $cmd₂) =>
    -- Limit ref variability for incrementality; see Note [Incremental Macros]
    withRef tk `(section $cmd₁:command $cmd₂ end)
  | _                 => Macro.throwUnsupported