inductive Lean.OpenDecl : Type

Data for representing open commands

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

instance Lean.instBEqOpenDecl : BEq OpenDecl

instance Lean.OpenDecl.instInhabited : Inhabited OpenDecl

instance Lean.OpenDecl.instToString : ToString OpenDecl

def Lean.rootNamespace : Name

def Lean.removeRoot (n : Name) : Name