inductive Lean.OpenDecl : Type

• simple: Lake.Name → List Lake.Name → Lean.OpenDecl
• explicit: Lake.Name → Lake.Name → Lean.OpenDecl

Data for representing open commands

instance Lean.instBEqOpenDecl : BEq Lean.OpenDecl

instance Lean.OpenDecl.instInhabitedOpenDecl : Inhabited Lean.OpenDecl

instance Lean.OpenDecl.instToStringOpenDecl : ToString Lean.OpenDecl

def Lean.rootNamespace : Lake.Name

def Lean.removeRoot (n : Lake.Name) : Lake.Name