# Zulip Chat Archive

## 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?

#### Leonardo de Moura (Mar 12 2021 at 20:28):

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`

.

#### Sebastian Ullrich (Mar 13 2021 at 12:21):

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

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

Thanks!

Last updated: May 18 2021 at 23:14 UTC