Lean.Class

source

structure Lean.ClassEntry :

Type

name : Lean.Name
hasOutParam : Bool

source

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

Bool

Equations

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

source

structure Lean.ClassState :

Type

hasOutParam : Lean.SMap Lean.Name Bool

source

instance Lean.instInhabitedClassState :

Inhabited Lean.ClassState

Equations

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

source

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 }

source

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

Lean.ClassState

Equations

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

source

constant Lean.classExtension :

Lean.SimplePersistentEnvExtension Lean.ClassEntry Lean.ClassState

source

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

Bool

Equations

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

source

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

Bool

Equations

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

source

def Lean.isOutParam (e : Lean.Expr) :

Bool

Equations

Lean.isOutParam e = Lean.Expr.isAppOfArity e `outParam 1

source

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

Except String Lean.Environment

Equations

Lean.addClass env clsName = if Lean.isClass env clsName = true then Except.error (toString "class has already been declared '" ++ toString clsName ++ toString "'") else match Lean.Environment.find? env clsName with | none => Except.error ("unknown declaration '" ++ toString clsName ++ "'") | some decl@h:(Lean.ConstantInfo.inductInfo x) => do let b ← Lean.checkOutParam 1 #[] (Lean.ConstantInfo.type decl) Except.ok (Lean.PersistentEnvExtension.addEntry Lean.classExtension env { name := clsName, hasOutParam := b }) | some x => Except.error ("invalid 'class', declaration '" ++ toString clsName ++ "' must be inductive datatype or structure")

source

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

Lean.Expr → Option Lean.Name