inductive Lean.OpenDecl : Type

Data for representing open commands

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

instance Lean.instBEqOpenDecl : BEq Lean.OpenDecl

Equations

• Lean.instBEqOpenDecl = { beq := Lean.beqOpenDecl✝ }

instance Lean.OpenDecl.instInhabited : Inhabited Lean.OpenDecl

Equations

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

instance Lean.OpenDecl.instToString : ToString Lean.OpenDecl

Equations

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

def Lean.rootNamespace : Lean.Name

Equations

• Lean.rootNamespace = `_root_

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

Equations

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