set_option ... in section, vs variable in section

Stream: lean4

[Adam Topaz]

I just came across something curious.
First, here's a bit of Lean4 code that does what is expected:

variable (α : Type u) in
set_option pp.universes true in section

#check α

end

It just shows α : Type u in the infoview at the #check location.
Now let's flip the set_option and variable commands:

set_option pp.universes true in
variable (α : Type u) in section

#check α

end

This results in an error at alpha: unknown identifier 'α'.

Now let's remove the set_option:

variable (α : Type u) in section

#check α

end

This again works, and shows α : Type u at the #check location.

What's going on?

[Damiano Testa]

I do not have an answer to your question, but I also discovered this. Which one do you think is correct?

section a in
  section
  end a
end

section a in
  section
  end
end a

(the indentation is unnecessary, but I thought that it was helpful!)

[Damiano Testa]

Also, if you type

section a in
section b

then I was unable to finish this in a way that Lean was happy!

[Damiano Testa]

I think that section closes early due to the end inserted by the in. If you do this:

universe u

variable (α : Type u) in
set_option pp.all true in
section
example {a : α} : 3 = 3 := rfl

depending on the order of the ins, you either do not get the pretty-printing or you do not have α in the example.

[Damiano Testa]

My guess is that <whatever> in section basically does nothing (except possibly consuming an end and never complaining about it).

[Kyle Miller]

Yeah, the X in Y is section X Y end, so if you do X in section you get section X section end.

This is a consequence to section and end being commands in their own right, rather than being some larger syntactic construct that collects all the commands between them.

[Mario Carneiro]

I'm thinking it would be best to just have in detect when the RHS is a section or namespace command and just elaborate A in B in section as section; A; B

[Kyle Miller]

I wonder if there should be two levels of commands, with section/namespace/end not being normal commands, which would allow X in section to not parse since section wouldn't be a normal command.

[Mario Carneiro]

It's easy enough to make X in section not parse if we want to go that route

[Mario Carneiro]

but do we want this to work?

[Kyle Miller]

I suppose we could make X in section foo expand to section foo X easily enough, but we'd want to be sure it works with multiple ins