source
inductive Lean.OpenDecl :
Type

Data for representing `open` commands

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

Instances For

source
instance Lean.instBEqOpenDecl :
BEq OpenDecl
Equations

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

source
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

Instances For

source
instance Lean.OpenDecl.instInhabited :
Inhabited OpenDecl
Equations

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

source
instance Lean.OpenDecl.instToString :
ToString OpenDecl
Equations

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

source
def Lean.rootNamespace :
Name
Equations

- Lean.rootNamespace = `_root_

Instances For

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

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

Instances For