Zulip Chat Archive

Stream: lean4

Topic: local notations


view this post on Zulip Jason Gross (Mar 12 2021 at 20:04):

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

view this post on Zulip Leonardo de Moura (Mar 12 2021 at 20:28):

Yes.

view this post on Zulip 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 ℕ?

view this post on Zulip 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

view this post on Zulip Leonardo de Moura (Mar 12 2021 at 20:37):

I will investigate.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Mar 13 2021 at 12:21):

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

view this post on Zulip Jason Gross (Mar 15 2021 at 17:48):

Thanks!


Last updated: May 18 2021 at 23:14 UTC