How to create a hidden namespace?

Stream: new members

[Yee-Jian Tan]

I have this simple MWE:

namespace hidden
notation:100 "ℕ" => Nat

axiom add : ℕ → ℕ → ℕ

variable (w x y z : ℕ)

#check add x y

local infixl:65 " + " => add

#check x + y

end hidden

the #check x+y returns

Ambiguous term
  x + y
Possible interpretations:
  x + y : ℕ

  x + y : ℕ

[Kenny Lau]

why are you redefining an existing infix?

[Yee-Jian Tan]

I guess the question should be: how can I create a hidden namespace, or forget/hide existing notations?

[Kenny Lau]

I could be wrong, but I don't think there's a way to remove a globally-defined notation in the prelude

[Kenny Lau]

i would suggest you modify the symbol e.g. +'

[Kenny Lau]

also I think another part of your problem is that you're still using the Nat instead of a new nat

[Kenny Lau]

namespace hidden
axiom myNat : Type
notation:100 "ℕ" => myNat

axiom add : ℕ → ℕ → ℕ

variable (w x y z : ℕ)

#check add x y

local infixl:65 " + " => add

#check x + y

end hidden

[Kenny Lau]

for example this works

[Yee-Jian Tan]

That's good to know. Still, is there a way to use the same Nat and the same symbol + ?

[Kenny Lau]

I don't think so.

[Alfredo Moreira-Rosa]

In case you don't know you can write your own instances of HAdd or Add typeclasses and evoid the issue of defining your own infix, and it will respect your hidden namespace

[Robin Arnez]

The thing to do with existing notation is not to redefine it but to create macro_rules:

variable (x y : Nat)

section

axiom add (a b : Nat) : Nat

local macro_rules
  | `($a + $b) => `(add $a $b)

@[app_unexpander add]
def unexpandAdd : Lean.PrettyPrinter.Unexpander
  | `($_ $a $b) => `($a + $b)
  | _ => throw ()

/-- info: x + y : Nat -/ #guard_msgs in
#check x + y

set_option pp.notation false in
/-- info: add x y : Nat -/ #guard_msgs in
#check x + y

end

/-- info: x + y : Nat -/ #guard_msgs in
#check x + y

set_option pp.notation false in
/-- info: HAdd.hAdd x y : Nat -/ #guard_msgs in
#check x + y

[Robin Arnez]

If you don't want to write the unexpander yourself or want more control over precedence etc., you can instead disable the existing notation:

local macro_rules
  | `($a + $b) => Lean.Macro.throwError "macro disabled"

local infixl:65 " + " => add

[Yee-Jian Tan]

Thanks! For pedagogical purposes, I decided to stick with another symbol (i.e. suffixed with ') instead, it would have been nice if we could disable these natively.