Scope of notation inside a namespace

Stream: new members

[Luiz Kazuo Takei]

Correct me if I am wrong but my understanding is that definitions inside a namespace have priority over definitions outside that namespace. So, for instance, the code below would work fine:

namespace TestSpace

-- yes, this definition is wrong but just for the sake of the example
def Even (n : ℕ) := ∃ (k : ℕ), n = 2*k + 1

example : Even 5 := by
  use 2

end TestSpace

Now I tried to do something similar for an infix notation (that clashes with a notation defined elsewhere in mathlib) and Lean gives me an error message saying that it is an ambiguous term. Here's the code:

namespace TestSpace

def Divides (a b : ℕ) := ∃ (k : ℕ), b = k*a

infix:99 "∣" => Divides

example : 5 ∣ 20 := by sorry

end Testspace

Why doesn't it use the notation defined in the namespace by default? Also, can I force it to use the definition inside the namespace?

[Mirek Olšák]

Notation and a name is quite a different thing. Notation is even global by default (still applicable after leaving the namespace but that can be changed with scoped notation). I am not sure if you can delete a default notation (some smarter people here could know).

Hovewer, a standard way of defining your own division is through implementing a custom Dvd typeclass (which can even handle ambiguous typeclass resolutions).

[Eric Paul]

Here are two options which are probably not the best but may be interesting. The first is changing priority and the second is removing the default notation as Mirek Olšák mentioned.

When two notations work equally well, Lean tries choosing the one with higher priority. The default priority is 1000, so by giving your notation any priority higher than that, it becomes the one Lean chooses to use:

import Mathlib

namespace TestSpace

def Divides (a b : ℕ) := ∃ (k : ℕ), b = k*a

infix:99 (priority := 1001) "∣" => Divides

example : 5 ∣ 20 := by sorry

end TestSpace

Now here is a way to remove previously existing notation and replace it with your own. I think this is probably unreasonable but is fun and emphasizes the fact that Lean's parser is entirely customizable.

import Mathlib
import Lean
open Lean Parser

-- For each first token of `p`, set list of relevant parsers to just be `p`
def setTrailingParser (tables : PrattParsingTables) (p : TrailingParser) (prio : Nat) :
    PrattParsingTables :=
  let addTokens (tks : List Token) : PrattParsingTables :=
    let tks := tks.map fun tk => Name.mkSimple tk
    tks.eraseDups.foldl (init := tables) fun tables tk =>
      { tables with trailingTable := Std.TreeMap.insert tables.trailingTable tk [(p, prio)] }
  match p.info.firstTokens with
  | FirstTokens.tokens tks    => addTokens tks
  | FirstTokens.optTokens tks => addTokens tks
  | _ => tables

elab "makeOnlyParser " p:ident : command => do
  let cats := parserExtension.getState (←getEnv) |>.categories
  let parserName ← resolveGlobalConstNoOverload p
  let (_, parser) ← Elab.Command.liftTermElabM <| mkParserOfConstant cats parserName
  modifyEnv fun env =>
    parserExtension.modifyState env fun state =>
        let termCat := state.categories.find! `term
        let newTables := setTrailingParser termCat.tables parser 1000
        let newCats := state.categories.insert `term {termCat with tables := newTables}
        {state with categories := newCats}

namespace TestSpace

def Divides (a b : ℕ) := ∃ (k : ℕ), b = k*a

infix:99 (name := myDiv) "∣" => Divides
makeOnlyParser myDiv

example : 5 ∣ 20 := by sorry
-- The default notation is gone in this namespace
example [Field α] (x y : α) : x ∣ y := by sorry

end TestSpace
-- Still works outside of this namespace
example [Field α] (x y : α) : x ∣ y := by sorry

[Luiz Kazuo Takei]

Thank you very much for the answers @Mirek Olšák and @Eric Paul !

@Eric Paul, the 1st solution works very well. The 2nd solution is interesting but way above my level... :joy: