inductive Lean.OpenDecl : Type

Data for representing open commands

• simple (ns : Name) (except : List Name) : OpenDecl
• explicit (id declName : Name) : OpenDecl

@[implicit_reducible]

instance Lean.instBEqOpenDecl : BEq OpenDecl

def Lean.instBEqOpenDecl.beq : OpenDecl → OpenDecl → Bool

@[implicit_reducible]

instance Lean.OpenDecl.instInhabited : Inhabited OpenDecl

@[implicit_reducible]

instance Lean.OpenDecl.instToString : ToString OpenDecl

def Lean.rootNamespace : Name

def Lean.removeRoot (n : Name) : Name