namespace confusion when inductive constructor has same name

Stream: new members

[Alok Singh]

inductive Paradox : Type
| True
| False
| Paradox

def Paradox.not (p : Paradox) : Paradox :=
  match p with
  | Paradox.Paradox => Paradox.Paradox
  | Paradox.False => Paradox.True
  | Paradox.True => Paradox.False

gives an error and trying to rename Paradox.Paradox to something else changed the inductive type and not just the constructor

[Alok Singh]

speaking of rename issues, trying to rename the type Paradox

inductive Paradox : Type
| True
| False
| Antimony

def Paradox.not: Paradox -> Paradox
  | .Antimony => .False
  | .False => .True
  | .True => .False

does not rename Paradox.not

[Adam Topaz]

When you write Paradox.not that opens the Paradox namespace. Here's a fix:

inductive Paradox : Type
| True
| False
| Paradox

def Paradox.not (p : _root_.Paradox) : _root_.Paradox :=
  match p with
  | Paradox.Paradox => Paradox.Paradox
  | Paradox.False => Paradox.True
  | Paradox.True => Paradox.False

[Adam Topaz]

Or even better:

inductive Paradox : Type
| true
| false
| paradox

def Paradox.not (p : Paradox) : Paradox :=
  match p with
  | .paradox => .paradox
  | .false => .true
  | .true => .false

[Alok Singh]

Ah, didn't know it opened it, thought makes sense. Thanks =)

[Kevin Buzzard]

It's really useful as well as being a footgun.