## Stream: lean4

### Topic: local notations

#### Jason Gross (Mar 12 2021 at 20:04):

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

Yes.

#### Jason Gross (Mar 12 2021 at 20:31):

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 (Mar 12 2021 at 20:33):

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 (Mar 12 2021 at 20:37):

I will investigate.

#### Leonardo de Moura (Mar 13 2021 at 03:55):

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 (Mar 13 2021 at 04:09):

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.

#### Jason Gross (Mar 15 2021 at 17:48):

Thanks!

Last updated: May 18 2021 at 23:14 UTC