structure Lean.ClassEntry : Type

An entry for the persistent environment extension for declared type classes

• name : Name

  Class name.

• outParams : Array Nat

  Position of the class outParams. For example, for class

  class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where
  

  outParams := #[2, 3]

• outLevelParams : Array Nat

  Positions of universe level parameters that only appear in output parameter types. For example, for HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)), outLevelParams := #[2] since universe w only appears in the output parameter γ. This is used to normalize TC resolution cache keys.

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

Equations

• a.lt b = a.name.quickLt b.name

structure Lean.ClassState : Type

State of the type class environment extension.

• outParamMap : SMap Name (Array Nat)
• outLevelParamMap : SMap Name (Array Nat)

@[instance_reducible]

instance Lean.instInhabitedClassState : Inhabited ClassState

Equations

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

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

Equations

• s.addEntry entry = { outParamMap := s.outParamMap.insert entry.name entry.outParams, outLevelParamMap := s.outLevelParamMap.insert entry.name entry.outLevelParams }

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

Switch the state into persistent mode. We switch to this mode after we read all imported .olean files. Recall that we use a SMap for implementing the state of the type class environment extension.

Equations

• s.switch = { outParamMap := s.outParamMap.switch, outLevelParamMap := s.outLevelParamMap.switch }

opaque Lean.classExtension : SimplePersistentEnvExtension ClassEntry ClassState

Type class environment extension

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

Return true if n is the name of type class in the given environment.

Equations

• Lean.isClass env n = (Lean.classExtension.getState env).outParamMap.contains n

def Lean.getOutParamPositions? (env : Environment) (declName : Name) : Option (Array Nat)

If declName is a class, return the position of its outParams.

Equations

• Lean.getOutParamPositions? env declName = (Lean.classExtension.getState env).outParamMap.find? declName

def Lean.hasOutParams (env : Environment) (declName : Name) : Bool

Return true if the given declName is a type class with output parameters.

Equations

• Lean.hasOutParams env declName = match Lean.getOutParamPositions? env declName with | some outParams => !outParams.isEmpty | none => false

def Lean.getOutLevelParamPositions? (env : Environment) (declName : Name) : Option (Array Nat)

If declName is a class, return the positions of universe level parameters that only appear in output parameter types.

Equations

• Lean.getOutLevelParamPositions? env declName = (Lean.classExtension.getState env).outLevelParamMap.find? declName

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

Add a new type class with the given name to the environment. declName must not be the name of an existing type class, and it must be the name of constant in env. declName must be a inductive datatype or axiom. Recall that all structures are inductive datatypes.

Equations

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