An entry for the persistent environment extension for declared type classes
- name : Lake.Name
Class name.
Instances For
Equations
- Lean.ClassEntry.lt a b = Lean.Name.quickLt a.name b.name
Instances For
Equations
- Lean.instInhabitedClassState = { default := { outParamMap := default } }
Equations
- Lean.ClassState.addEntry s entry = { outParamMap := Lean.SMap.insert s.outParamMap entry.name entry.outParams }
Instances For
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
- Lean.ClassState.switch s = { outParamMap := Lean.SMap.switch s.outParamMap }
Instances For
Type class environment extension
Return true
if n
is the name of type class in the given environment.
Equations
- Lean.isClass env n = Lean.SMap.contains (Lean.SimplePersistentEnvExtension.getState Lean.classExtension env).outParamMap n
Instances For
If declName
is a class, return the position of its outParams
.
Equations
- Lean.getOutParamPositions? env declName = Lean.SMap.find? (Lean.SimplePersistentEnvExtension.getState Lean.classExtension env).outParamMap declName
Instances For
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 => !Array.isEmpty outParams | none => false
Instances For
Mark outParam
s in type
as implicit. Note that it also marks instance implicit arguments that depend on outParam
s as implicit.
Remark: this function consumes the outParam
annotations.
This function uses the same logic used as checkOutParam
.
See issue #1901
Equations
- Lean.mkOutParamArgsImplicit type = Lean.mkOutParamArgsImplicit.go type type #[]
Instances For
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.