local notations

Stream: lean4

[Jason Gross]

local notation is supposed to disappear at the end of a section, right?

[Leonardo de Moura]

Yes.

[Jason Gross]

Hm, I hit a case where they don't (perhaps because I set_option hygiene false in the section?), but I'm struggling to minimize it because I can't seem to get small examples of notations working at all.

notation "ℕ" => Nat
#check ℕ -- Nat : Type  -- why not print ℕ?

[Jason Gross]

Hm, local notation seems to just not disappear after sections?

axiom n : Type → Type
section
local notation "ℕ" x => n x
end
#check n Nat -- ℕ Nat : Type

[Leonardo de Moura]

I will investigate.

[Leonardo de Moura]

Jason Gross said:

Hm, I hit a case where they don't (perhaps because I set_option hygiene false in the section?), but I'm struggling to minimize it because I can't seem to get small examples of notations working at all.

notation "ℕ" => Nat
#check ℕ -- Nat : Type  -- why not print ℕ?

Fixed this one.

[Leonardo de Moura]

Jason Gross said:

Hm, local notation seems to just not disappear after sections?

axiom n : Type → Type
section
local notation "ℕ" x => n x
end
#check n Nat -- ℕ Nat : Type

I found the problem with this one but didn't fix yet. The parser is scoped, but the pretty printer is not :(
Note that #check ℕ Nat is a syntax error after the end.

[Sebastian Ullrich]

Fixed in https://github.com/leanprover/lean4/commit/00a0db4231156fbdd0e316b9ce0b2d1c301aa74f

[Jason Gross]

Thanks!