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

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

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