duplicate namespace and declaration

Stream: lean4

[Paige Thomas]

I have some function names that overlap, but are about different things. For example, I have kleene_closure, where in one case it refers to strings and in the other to languages. In a similar manner I have derivative, where in one case it refers to languages and in the other it refers to regular expressions. I was managing this by putting them into different namespaces, Strings, Languages, RegExp, but I also have types defined with those names. For example

namespace RegExp


inductive RegExp (α : Type) : Type
  | char : α → RegExp α
  | epsilon : RegExp α
  | zero : RegExp α
  | union : RegExp α → RegExp α → RegExp α
  | concat : RegExp α → RegExp α → RegExp α
  | kleene_closure : RegExp α → RegExp α
  deriving Inhabited, DecidableEq

α : Type
⊢ Sort ?u.3
Messages (1)
RegExp.lean:14:10
The namespace 'RegExp' is duplicated in the declaration 'RegExp.RegExp'
note: this linter can be disabled with `set_option linter.dupNamespace false`

The linter does not appear to like this. I could turn off the linter, or slightly change one of the names, but I'm wondering if there is another way to address this, or something canonical.

[Daniel Weber]

You can move the type outside of the namespace - the constructors would still be e.g. RegExp.kleene_closure

[Paige Thomas]

I think I tried that, and something went wrong, but I forget what. I'll try again.

[Paige Thomas]

Ok, this is what happened when I moved the inductive definition of Language outside of the namespace Language. In another file that transitively imports the file containing that definition, I have

namespace Language

def Language.is_nullable
  {α : Type}
  (L : Language α) :
  Prop :=
  [] ∈ L

because I want to do things like

lemma is_nullable_iff_nullify_eq_eps_singleton
  {α : Type}
  [DecidableEq α]
  (L : Language α) :
  L.is_nullable ↔ L.nullify = {[]} :=

where I have L.is_nullable instead of Language.is_nullable L. But I didn't realize I could still do the same thing if I removed the Language. prefix from the definition.

namespace Language

def is_nullable
  {α : Type}
  (L : Language α) :
  Prop :=
  [] ∈ L

lemma is_nullable_iff_nullify_eq_eps_singleton
  {α : Type}
  [DecidableEq α]
  (L : Language α) :
  L.is_nullable ↔ L.nullify = {[]} :=

So I think that works. Thank you.

[Thomas Murrills]

I think moving the type outside the namespace like that is intended to be the canonical pattern here, as that lets you define foo (a : RegExp A) : ... within namespace RegExp later on and call it on any x : RegExp A with dot syntax (x.foo).

[Paige Thomas]

Thank you!