Documentation

Lean.Declaration

inductive Lean.ReducibilityHints:

Type

opaque: Lean.ReducibilityHints
abbrev: Lean.ReducibilityHints
regular: UInt32 → Lean.ReducibilityHints

Reducibility hints are used in the convertibility checker. When trying to solve a constraint such a

       (f ...) =?= (g ...)

where f and g are definitions, the checker has to decide which one will be unfolded. If f (g) is opaque, then g (f) is unfolded if it is also not marked as opaque, Else if f (g) is abbrev, then f (g) is unfolded if g (f) is also not marked as abbrev, Else if f and g are regular, then we unfold the one with the biggest definitional height. Otherwise both are unfolded.

The arguments of the regular Constructor are: the definitional height and the flag selfOpt.

The definitional height is by default computed by the kernel. It only takes into account other regular definitions used in a definition. When creating declarations using meta-programming, we can specify the definitional depth manually.

Remark: the hint only affects performance. None of the hints prevent the kernel from unfolding a declaration during Type checking.

Remark: the ReducibilityHints are not related to the attributes: reducible/irrelevance/semireducible. These attributes are used by the Elaborator. The ReducibilityHints are used by the kernel (and Elaborator). Moreover, the ReducibilityHints cannot be changed after a declaration is added to the kernel.

instance Lean.instInhabitedReducibilityHints:

Inhabited Lean.ReducibilityHints

Equations

Lean.instInhabitedReducibilityHints = { default := Lean.ReducibilityHints.opaque }

@[export lean_mk_reducibility_hints_regular]

def Lean.mkReducibilityHintsRegularEx (h : UInt32) :

Lean.ReducibilityHints

Equations

Lean.mkReducibilityHintsRegularEx h = Lean.ReducibilityHints.regular h

@[export lean_reducibility_hints_get_height]

def Lean.ReducibilityHints.getHeightEx (h : Lean.ReducibilityHints) :

Equations

Lean.ReducibilityHints.getHeightEx h = match h with | Lean.ReducibilityHints.regular h => h | x => 0

def Lean.ReducibilityHints.lt:

Lean.ReducibilityHints → Lean.ReducibilityHints → Bool

Equations

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

def Lean.ReducibilityHints.isAbbrev:

Lean.ReducibilityHints → Bool

Equations

Lean.ReducibilityHints.isAbbrev _fun_discr = match _fun_discr with | Lean.ReducibilityHints.abbrev => true | x => false

def Lean.ReducibilityHints.isRegular:

Lean.ReducibilityHints → Bool

Equations

Lean.ReducibilityHints.isRegular _fun_discr = match _fun_discr with | Lean.ReducibilityHints.regular a => true | x => false

structure Lean.ConstantVal:

Type

name : Lean.Name
levelParams : List Lean.Name
type : Lean.Expr

Base structure for AxiomVal, DefinitionVal, TheoremVal, InductiveVal, ConstructorVal, RecursorVal and QuotVal.

instance Lean.instInhabitedConstantVal:

Inhabited Lean.ConstantVal

Equations

Lean.instInhabitedConstantVal = { default := { name := default, levelParams := default, type := default } }

structure Lean.AxiomValextends Lean.ConstantVal :

Type

isUnsafe : Bool

instance Lean.instInhabitedAxiomVal:

Inhabited Lean.AxiomVal

Equations

Lean.instInhabitedAxiomVal = { default := { toConstantVal := default, isUnsafe := default } }

@[export lean_mk_axiom_val]

def Lean.mkAxiomValEx (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (isUnsafe : Bool) :

Equations

Lean.mkAxiomValEx name levelParams type isUnsafe = { toConstantVal := { name := name, levelParams := levelParams, type := type }, isUnsafe := isUnsafe }

@[export lean_axiom_val_is_unsafe]

def Lean.AxiomVal.isUnsafeEx (v : Lean.AxiomVal) :

Equations

Lean.AxiomVal.isUnsafeEx v = v.isUnsafe

inductive Lean.DefinitionSafety:

Type

instance Lean.instInhabitedDefinitionSafety:

Inhabited Lean.DefinitionSafety

Equations

Lean.instInhabitedDefinitionSafety = { default := Lean.DefinitionSafety.unsafe }

instance Lean.instBEqDefinitionSafety:

BEq Lean.DefinitionSafety

Equations

Lean.instBEqDefinitionSafety = { beq := [anonymous] }

instance Lean.instReprDefinitionSafety:

Repr Lean.DefinitionSafety

Equations

Lean.instReprDefinitionSafety = { reprPrec := [anonymous] }

structure Lean.DefinitionValextends Lean.ConstantVal :

Type

value : Lean.Expr
hints : Lean.ReducibilityHints
safety : Lean.DefinitionSafety
List of all (including this one) declarations in the same mutual block. Note that this information is not used by the kernel, and is only used to save the information provided by the user when using mutual blocks. Recall that the Lean kernel does not support recursive definitions and they are compiled using recursors and WellFounded.fix.
all : List Lean.Name

instance Lean.instInhabitedDefinitionVal:

Inhabited Lean.DefinitionVal

Equations

Lean.instInhabitedDefinitionVal = { default := { toConstantVal := default, value := default, hints := default, safety := default, all := default } }

@[export lean_mk_definition_val]

def Lean.mkDefinitionValEx (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (value : Lean.Expr) (hints : Lean.ReducibilityHints) (safety : Lean.DefinitionSafety) (all : List Lean.Name) :

Lean.DefinitionVal

Equations

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

@[export lean_definition_val_get_safety]

def Lean.DefinitionVal.getSafetyEx (v : Lean.DefinitionVal) :

Lean.DefinitionSafety

Equations

Lean.DefinitionVal.getSafetyEx v = v.safety

structure Lean.TheoremValextends Lean.ConstantVal :

Type

value : Lean.Expr
List of all (including this one) declarations in the same mutual block. See comment at DefinitionVal.all.
all : List Lean.Name

instance Lean.instInhabitedTheoremVal:

Inhabited Lean.TheoremVal

Equations

Lean.instInhabitedTheoremVal = { default := { toConstantVal := default, value := default, all := default } }

structure Lean.OpaqueValextends Lean.ConstantVal :

Type

value : Lean.Expr
isUnsafe : Bool
List of all (including this one) declarations in the same mutual block. See comment at DefinitionVal.all.
all : List Lean.Name

instance Lean.instInhabitedOpaqueVal:

Inhabited Lean.OpaqueVal

Equations

Lean.instInhabitedOpaqueVal = { default := { toConstantVal := default, value := default, isUnsafe := default, all := default } }

@[export lean_mk_opaque_val]

def Lean.mkOpaqueValEx (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (value : Lean.Expr) (isUnsafe : Bool) (all : List Lean.Name) :

Equations

Lean.mkOpaqueValEx name levelParams type value isUnsafe all = { toConstantVal := { name := name, levelParams := levelParams, type := type }, value := value, isUnsafe := isUnsafe, all := all }

@[export lean_opaque_val_is_unsafe]

def Lean.OpaqueVal.isUnsafeEx (v : Lean.OpaqueVal) :

Equations

Lean.OpaqueVal.isUnsafeEx v = v.isUnsafe

structure Lean.Constructor:

Type

name : Lean.Name
type : Lean.Expr

instance Lean.instInhabitedConstructor:

Inhabited Lean.Constructor

Equations

Lean.instInhabitedConstructor = { default := { name := default, type := default } }

structure Lean.InductiveType:

Type

instance Lean.instInhabitedInductiveType:

Inhabited Lean.InductiveType

Equations

Lean.instInhabitedInductiveType = { default := { name := default, type := default, ctors := default } }

inductive Lean.Declaration:

Type

axiomDecl: Lean.AxiomVal → Lean.Declaration
defnDecl: Lean.DefinitionVal → Lean.Declaration
thmDecl: Lean.TheoremVal → Lean.Declaration
opaqueDecl: Lean.OpaqueVal → Lean.Declaration
quotDecl: Lean.Declaration
mutualDefnDecl: List Lean.DefinitionVal → Lean.Declaration
inductDecl: List Lean.Name → Nat → List Lean.InductiveType → Bool → Lean.Declaration

Declaration object that can be sent to the kernel.

instance Lean.instInhabitedDeclaration:

Inhabited Lean.Declaration

Equations

Lean.instInhabitedDeclaration = { default := Lean.Declaration.axiomDecl default }

@[export lean_mk_inductive_decl]

def Lean.mkInductiveDeclEs (lparams : List Lean.Name) (nparams : Nat) (types : List Lean.InductiveType) (isUnsafe : Bool) :

Lean.Declaration

Equations

Lean.mkInductiveDeclEs lparams nparams types isUnsafe = Lean.Declaration.inductDecl lparams nparams types isUnsafe

@[export lean_is_unsafe_inductive_decl]

def Lean.Declaration.isUnsafeInductiveDeclEx:

Lean.Declaration → Bool

Equations

Lean.Declaration.isUnsafeInductiveDeclEx _fun_discr = match _fun_discr with | Lean.Declaration.inductDecl lparams nparams types isUnsafe => isUnsafe | x => false

@[specialize]

def Lean.Declaration.foldExprM {α : Type} {m : Type → Type} [inst : Monad m] (d : Lean.Declaration) (f : α → Lean.Expr → m α) (a : α) :

m α

Equations

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

@[inline]

def Lean.Declaration.forExprM {m : Type → Type} [inst : Monad m] (d : Lean.Declaration) (f : Lean.Expr → m Unit) :

Equations

Lean.Declaration.forExprM d f = Lean.Declaration.foldExprM d (fun x a => f a) ()

structure Lean.InductiveValextends Lean.ConstantVal :

Type

Number of parameters. A parameter is an argument to the defined type that is fixed over constructors.
numParams : Nat
Number of indices. An index is an argument that varies over constructors.
An example of this is the n : Nat argument in the vector constructor cons : α → Vector α n → Vector α (n+1)
numIndices : Nat
List of all (including this one) inductive datatypes in the mutual declaration containing this one
all : List Lean.Name
List of the names of the constructors for this inductive datatype.
ctors : List Lean.Name
true when recursive (that is, the inductive type appears as an argument in a constructor).
isRec : Bool
Whether the definition is flagged as unsafe.
isUnsafe : Bool
isReflexive : Bool
An inductive definition T is nested when there is a constructor with an argument x : F T, where F : Type → Type is some suitably behaved (ie strictly positive) function (Eg Array T, List T, T × T, ...).
isNested : Bool

The kernel compiles (mutual) inductive declarations (see inductiveDecls) into a set of - Declaration.inductDecl (for each inductive datatype in the mutual Declaration), - Declaration.ctorDecl (for each Constructor in the mutual Declaration), - Declaration.recDecl (automatically generated recursors).

This data is used to implement iota-reduction efficiently and compile nested inductive
declarations.

A series of checks are performed by the kernel to check whether a `inductiveDecls`
is valid or not.

instance Lean.instInhabitedInductiveVal:

Inhabited Lean.InductiveVal

Equations

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

@[export lean_mk_inductive_val]

def Lean.mkInductiveValEx (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (numParams : Nat) (numIndices : Nat) (all : List Lean.Name) (ctors : List Lean.Name) (isRec : Bool) (isUnsafe : Bool) (isReflexive : Bool) (isNested : Bool) :

Lean.InductiveVal

Equations

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

@[export lean_inductive_val_is_rec]

def Lean.InductiveVal.isRecEx (v : Lean.InductiveVal) :

Equations

Lean.InductiveVal.isRecEx v = v.isRec

@[export lean_inductive_val_is_unsafe]

def Lean.InductiveVal.isUnsafeEx (v : Lean.InductiveVal) :

Equations

Lean.InductiveVal.isUnsafeEx v = v.isUnsafe

@[export lean_inductive_val_is_reflexive]

def Lean.InductiveVal.isReflexiveEx (v : Lean.InductiveVal) :

Equations

Lean.InductiveVal.isReflexiveEx v = v.isReflexive

@[export lean_inductive_val_is_nested]

def Lean.InductiveVal.isNestedEx (v : Lean.InductiveVal) :

Equations

Lean.InductiveVal.isNestedEx v = v.isNested

def Lean.InductiveVal.numCtors (v : Lean.InductiveVal) :

Equations

Lean.InductiveVal.numCtors v = List.length v.ctors

structure Lean.ConstructorValextends Lean.ConstantVal :

Type

Inductive type this constructor is a member of
induct : Lean.Name
Constructor index (i.e., Position in the inductive declaration)
cidx : Nat
Number of parameters in inductive datatype.
numParams : Nat
Number of fields (i.e., arity - nparams)
numFields : Nat
isUnsafe : Bool

instance Lean.instInhabitedConstructorVal:

Inhabited Lean.ConstructorVal

Equations

Lean.instInhabitedConstructorVal = { default := { toConstantVal := default, induct := default, cidx := default, numParams := default, numFields := default, isUnsafe := default } }

@[export lean_mk_constructor_val]

def Lean.mkConstructorValEx (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (induct : Lean.Name) (cidx : Nat) (numParams : Nat) (numFields : Nat) (isUnsafe : Bool) :

Lean.ConstructorVal

Equations

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

@[export lean_constructor_val_is_unsafe]

def Lean.ConstructorVal.isUnsafeEx (v : Lean.ConstructorVal) :

Equations

Lean.ConstructorVal.isUnsafeEx v = v.isUnsafe

structure Lean.RecursorRule:

Type

Reduction rule for this Constructor
ctor : Lean.Name
Number of fields (i.e., without counting inductive datatype parameters)
nfields : Nat
Right hand side of the reduction rule
rhs : Lean.Expr

Information for reducing a recursor

instance Lean.instInhabitedRecursorRule:

Inhabited Lean.RecursorRule

Equations

Lean.instInhabitedRecursorRule = { default := { ctor := default, nfields := default, rhs := default } }

structure Lean.RecursorValextends Lean.ConstantVal :

Type

List of all inductive datatypes in the mutual declaration that generated this recursor
all : List Lean.Name
Number of parameters
numParams : Nat
Number of indices
numIndices : Nat
Number of motives
numMotives : Nat
Number of minor premises
numMinors : Nat
A reduction for each Constructor
rules : List Lean.RecursorRule
It supports K-like reduction
k : Bool
isUnsafe : Bool

instance Lean.instInhabitedRecursorVal:

Inhabited Lean.RecursorVal

Equations

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

@[export lean_mk_recursor_val]

def Lean.mkRecursorValEx (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (all : List Lean.Name) (numParams : Nat) (numIndices : Nat) (numMotives : Nat) (numMinors : Nat) (rules : List Lean.RecursorRule) (k : Bool) (isUnsafe : Bool) :

Lean.RecursorVal

Equations

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

@[export lean_recursor_k]

def Lean.RecursorVal.kEx (v : Lean.RecursorVal) :

Equations

Lean.RecursorVal.kEx v = v.k

@[export lean_recursor_is_unsafe]

def Lean.RecursorVal.isUnsafeEx (v : Lean.RecursorVal) :

Equations

Lean.RecursorVal.isUnsafeEx v = v.isUnsafe

def Lean.RecursorVal.getMajorIdx (v : Lean.RecursorVal) :

Equations

Lean.RecursorVal.getMajorIdx v = v.numParams + v.numMotives + v.numMinors + v.numIndices

def Lean.RecursorVal.getFirstIndexIdx (v : Lean.RecursorVal) :

Equations

Lean.RecursorVal.getFirstIndexIdx v = v.numParams + v.numMotives + v.numMinors

def Lean.RecursorVal.getFirstMinorIdx (v : Lean.RecursorVal) :

Equations

Lean.RecursorVal.getFirstMinorIdx v = v.numParams + v.numMotives

def Lean.RecursorVal.getInduct (v : Lean.RecursorVal) :

Equations

Lean.RecursorVal.getInduct v = Lean.Name.getPrefix v.toConstantVal.name

inductive Lean.QuotKind:

Type

instance Lean.instInhabitedQuotKind:

Inhabited Lean.QuotKind

Equations

Lean.instInhabitedQuotKind = { default := Lean.QuotKind.type }

structure Lean.QuotValextends Lean.ConstantVal :

Type

kind : Lean.QuotKind

instance Lean.instInhabitedQuotVal:

Inhabited Lean.QuotVal

Equations

Lean.instInhabitedQuotVal = { default := { toConstantVal := default, kind := default } }

@[export lean_mk_quot_val]

def Lean.mkQuotValEx (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr) (kind : Lean.QuotKind) :

Equations

Lean.mkQuotValEx name levelParams type kind = { toConstantVal := { name := name, levelParams := levelParams, type := type }, kind := kind }

@[export lean_quot_val_kind]

def Lean.QuotVal.kindEx (v : Lean.QuotVal) :

Equations

Lean.QuotVal.kindEx v = v.kind

inductive Lean.ConstantInfo:

Type

axiomInfo: Lean.AxiomVal → Lean.ConstantInfo
defnInfo: Lean.DefinitionVal → Lean.ConstantInfo
thmInfo: Lean.TheoremVal → Lean.ConstantInfo
opaqueInfo: Lean.OpaqueVal → Lean.ConstantInfo
quotInfo: Lean.QuotVal → Lean.ConstantInfo
inductInfo: Lean.InductiveVal → Lean.ConstantInfo
ctorInfo: Lean.ConstructorVal → Lean.ConstantInfo
recInfo: Lean.RecursorVal → Lean.ConstantInfo

Information associated with constant declarations.

instance Lean.instInhabitedConstantInfo:

Inhabited Lean.ConstantInfo

Equations

Lean.instInhabitedConstantInfo = { default := Lean.ConstantInfo.axiomInfo default }

def Lean.ConstantInfo.toConstantVal:

Lean.ConstantInfo → Lean.ConstantVal

Equations

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

def Lean.ConstantInfo.isUnsafe:

Lean.ConstantInfo → Bool

Equations

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

def Lean.ConstantInfo.name (d : Lean.ConstantInfo) :

Equations

Lean.ConstantInfo.name d = (Lean.ConstantInfo.toConstantVal d).name

def Lean.ConstantInfo.levelParams (d : Lean.ConstantInfo) :

Equations

Lean.ConstantInfo.levelParams d = (Lean.ConstantInfo.toConstantVal d).levelParams

def Lean.ConstantInfo.numLevelParams (d : Lean.ConstantInfo) :

Equations

Lean.ConstantInfo.numLevelParams d = List.length (Lean.ConstantInfo.levelParams d)

def Lean.ConstantInfo.type (d : Lean.ConstantInfo) :

Equations

Lean.ConstantInfo.type d = (Lean.ConstantInfo.toConstantVal d).type

def Lean.ConstantInfo.value?:

Lean.ConstantInfo → Option Lean.Expr

Equations

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

def Lean.ConstantInfo.hasValue:

Lean.ConstantInfo → Bool

Equations

Lean.ConstantInfo.hasValue _fun_discr = match _fun_discr with | Lean.ConstantInfo.defnInfo val => true | Lean.ConstantInfo.thmInfo val => true | x => false

def Lean.ConstantInfo.value!:

Lean.ConstantInfo → Lean.Expr

Equations

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

def Lean.ConstantInfo.hints:

Lean.ConstantInfo → Lean.ReducibilityHints

Equations

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

def Lean.ConstantInfo.isCtor:

Lean.ConstantInfo → Bool

Equations

Lean.ConstantInfo.isCtor _fun_discr = match _fun_discr with | Lean.ConstantInfo.ctorInfo val => true | x => false

def Lean.ConstantInfo.isInductive:

Lean.ConstantInfo → Bool

Equations

Lean.ConstantInfo.isInductive _fun_discr = match _fun_discr with | Lean.ConstantInfo.inductInfo val => true | x => false

def Lean.ConstantInfo.all:

Lean.ConstantInfo → List Lean.Name

List of all (including this one) declarations in the same mutual block.

Equations

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

@[extern lean_instantiate_type_lparams]

opaque Lean.ConstantInfo.instantiateTypeLevelParams (c : Lean.ConstantInfo) (ls : List Lean.Level) :

@[extern lean_instantiate_value_lparams]

opaque Lean.ConstantInfo.instantiateValueLevelParams (c : Lean.ConstantInfo) (ls : List Lean.Level) :

def Lean.mkRecName (declName : Lean.Name) :

Equations

Lean.mkRecName declName = Lean.Name.mkStr declName "rec"