inductive Lean.OpenDecl : Type

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

Data for representing open commands

instance Lean.OpenDecl.instInhabitedOpenDecl : Inhabited Lean.OpenDecl

Equations

• Lean.OpenDecl.instInhabitedOpenDecl = { default := Lean.OpenDecl.simple Lean.Name.anonymous [] }

instance Lean.OpenDecl.instToStringOpenDecl : ToString Lean.OpenDecl

Equations

• One or more equations did not get rendered due to their size.

def Lean.rootNamespace : Lean.Name

Equations

• Lean.rootNamespace = Lean.Name.mkStr1 "_root_"

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

Equations

• Lean.removeRoot n = Lean.Name.replacePrefix n Lean.rootNamespace Lean.Name.anonymous