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

Equations

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

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

Equations

• Lean.instBEqOpenDecl.beq (Lean.OpenDecl.simple a a_1) (Lean.OpenDecl.simple b b_1) = (a == b && a_1 == b_1)
• Lean.instBEqOpenDecl.beq (Lean.OpenDecl.explicit a a_1) (Lean.OpenDecl.explicit b b_1) = (a == b && a_1 == b_1)
• Lean.instBEqOpenDecl.beq x✝¹ x✝ = false

instance Lean.OpenDecl.instInhabited : Inhabited OpenDecl

Equations

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

instance Lean.OpenDecl.instToString : ToString OpenDecl

Equations

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

def Lean.rootNamespace : Name

Equations

• Lean.rootNamespace = `_root_

def Lean.removeRoot (n : Name) : Name

Equations

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