Documentation

Lean.Class

structure Lean.ClassEntry:

Type

name : Lean.Name
hasOutParam : Bool

def Lean.ClassEntry.lt (a : Lean.ClassEntry) (b : Lean.ClassEntry) :

Equations

Lean.ClassEntry.lt a b = Lean.Name.quickLt a.name b.name

structure Lean.ClassState:

Type

hasOutParam : Lean.SMap Lean.Name Bool

instance Lean.instInhabitedClassState:

Inhabited Lean.ClassState

Equations

Lean.instInhabitedClassState = { default := { hasOutParam := default } }

def Lean.ClassState.addEntry (s : Lean.ClassState) (entry : Lean.ClassEntry) :

Lean.ClassState

Equations

Lean.ClassState.addEntry s entry = { hasOutParam := Lean.SMap.insert s.hasOutParam entry.name entry.hasOutParam }

def Lean.ClassState.switch (s : Lean.ClassState) :

Lean.ClassState

Equations

Lean.ClassState.switch s = { hasOutParam := Lean.SMap.switch s.hasOutParam }

opaque Lean.classExtension:

Lean.SimplePersistentEnvExtension Lean.ClassEntry Lean.ClassState

@[export lean_is_class]

def Lean.isClass (env : Lean.Environment) (n : Lean.Name) :

Equations

Lean.isClass env n = Lean.SMap.contains (Lean.SimplePersistentEnvExtension.getState Lean.classExtension env).hasOutParam n

@[export lean_has_out_params]

def Lean.hasOutParams (env : Lean.Environment) (n : Lean.Name) :

Equations

Lean.hasOutParams env n = match Lean.SMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.classExtension env).hasOutParam n with | some b => b | none => false

def Lean.addClass (env : Lean.Environment) (clsName : Lean.Name) :

Except String Lean.Environment

Equations

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

partial def Lean.getClassName (env : Lean.Environment) :

Lean.Expr → Option Lean.Name