unhygienic notation + delab

Stream: lean4

[James Gallicchio]

I'm doing some PL formalization (a mistake). I want to have an unhygienic

set_option hygiene false in
infix:35 " ⊢ " => Entails

before declaring the Entails type:

inductive Entails {P : Type u} : Bunch P → Typ P → Prop
| ...

But after that declaration, I'd like an auto-generated delaborator for the syntax... how to do it? It seems like making the notation local causes the inductive to fail to compile (will put together an MWE)

[James Gallicchio]

section

set_option hygiene false in
local infix:30 " ⊢ " => Entails

inductive Entails : String → String → Prop
| hi : "hi" ⊢ "hi"  -- unexpected token '⊢'; expected command

end

infix:30 " ⊢ " => Entails
example : "bye" ⊢ "what" := sorry

[Kyle Miller]

The in combinator can be very confusing: it's wrapping both commands in a fresh section, so the inductive never sees that local notation.

[James Gallicchio]

i .. i see

[James Gallicchio]

set_option hygiene false in
section

local infix:30 " ⊢ " => Entails

inductive Entails : String → String → Prop
| hi : "hi" ⊢ "hi"

end

infix:30 " ⊢ " => Entails
example : "bye" ⊢ "what" := sorry

works. thanks kyle :)

[Mario Carneiro]

@James Gallicchio That construct is also evil, but it works exactly as one would hope so it's hard to say that it's wrong. What actually happens when you do set_option hygiene false in section is that it expands, as normal, to

section
set_option hygiene false
section
end

but the section you wrote matches with the end from the macro expansion resulting in an empty section, and the first section from the macro expansion matches with the end that you wrote further down. It all works out, but it's a bit reminiscent of C preprocessor macros that expand to an open brace...

[Mario Carneiro]

my alternative suggestion would be to just write section; set_option hygiene false instead

[Mario Carneiro]

I suppose a concrete thing to point to for why this is maybe not optimal is that you can't write

set_option hygiene false in
section foo

...

end foo

[Marcus Rossel]

Mario Carneiro said:

I suppose a concrete thing to point to for why this is maybe not optimal is that you can't write

set_option hygiene false in
section foo

...

end foo

Would it be unreasonable to change the behavior of in to actually work the way one intuitively expects in this case (i.e. when followed by a section)?

[Mario Carneiro]

I would like to overhaul the whole implementation, I don't think the mini section is the right semantics for quite a lot of cases of in

[Kyle Miller]

Something that would be nice is if the commands in in could know they are in in, like in set_attribute [instance] Foo in ... you'd want that to either raise an error that this is certainly not what you want or act like set_attribute [local instance] Foo automatically.

[Kyle Miller]

(Maybe you're thinking about overhauling it by making it so what comes before in is a new class of commands, in which case this is more straightforward. Otherwise, there would need to be some CommandElabM state recording whether we're in an in.)