Documentation

Lean.Data.OpenDecl

inductive Lean.OpenDecl :

Type

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

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

Lean.OpenDecl.instToStringOpenDecl = { toString := fun decl => match decl with | Lean.OpenDecl.explicit id decl => toString id ++ " → " ++ toString decl | Lean.OpenDecl.simple ns ex => toString ns ++ if (ex == []) = true then "" else " hiding " ++ toString ex }

def Lean.rootNamespace :

Equations

Lean.rootNamespace = `_root_

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

Equations

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