# Documentation

Lean.Declaration

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.

Instances For
Equations
@[export lean_mk_reducibility_hints_regular]
Equations
@[export lean_reducibility_hints_get_height]
Equations
• = match h with | => h | x => 0
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x with | Lean.ReducibilityHints.abbrev => true | x => false
Equations
• = match x with | => true | x => false

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

Instances For
Equations
structure Lean.AxiomValextends :
Instances For
Equations
@[export lean_mk_axiom_val]
def Lean.mkAxiomValEx (name : Lean.Name) (levelParams : ) (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]
Equations
• = v.isUnsafe
Equations
Equations
structure Lean.DefinitionValextends :
• value : Lean.Expr
• 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 :
Instances For
Equations
@[export lean_mk_definition_val]
def Lean.mkDefinitionValEx (name : Lean.Name) (levelParams : ) (type : Lean.Expr) (value : Lean.Expr) (hints : Lean.ReducibilityHints) (safety : Lean.DefinitionSafety) (all : ) :
Equations
• One or more equations did not get rendered due to their size.
@[export lean_definition_val_get_safety]
Equations
• = v.safety
structure Lean.TheoremValextends :
• value : Lean.Expr
• List of all (including this one) declarations in the same mutual block. See comment at DefinitionVal.all.

all :
Instances For
Equations
structure Lean.OpaqueValextends :
• value : Lean.Expr
• isUnsafe : Bool
• List of all (including this one) declarations in the same mutual block. See comment at DefinitionVal.all.

all :

Value for an opaque constant declaration opaque x : t := e

Instances For
Equations
@[export lean_mk_opaque_val]
def Lean.mkOpaqueValEx (name : Lean.Name) (levelParams : ) (type : Lean.Expr) (value : Lean.Expr) (isUnsafe : Bool) (all : ) :
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]
Equations
• = v.isUnsafe
Instances For
Equations
Instances For
Equations
• axiomDecl:
• defnDecl:
• thmDecl:
• opaqueDecl:
• quotDecl: Lean.Declaration
• mutualDefnDecl:
• inductDecl:

Declaration object that can be sent to the kernel.

Instances For
@[export lean_mk_inductive_decl]
def Lean.mkInductiveDeclEs (lparams : ) (nparams : Nat) (types : ) (isUnsafe : Bool) :
Equations
@[export lean_is_unsafe_inductive_decl]
Equations
@[specialize #[]]
def Lean.Declaration.foldExprM {α : Type} {m : } [inst : ] (d : Lean.Declaration) (f : αLean.Exprm α) (a : α) :
m α
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Declaration.forExprM {m : } [inst : ] (d : Lean.Declaration) (f : ) :
Equations
structure Lean.InductiveValextends :
• Number of parameters. A parameter is an argument to the defined type that is fixed over constructors. An example of this is the α : Type argument in the vector constructors nil : Vector α 0 and cons : α → Vector α n → Vector α (n+1)→ Vector α n → Vector α (n+1)→ Vector α (n+1).

The intuition is that the inductive type must exhibit parametric polymorphism over the inductive parameter, as opposed to ad-hoc polymorphism.

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)→ Vector α n → Vector α (n+1)→ Vector α (n+1).

numIndices : Nat
• List of all (including this one) inductive datatypes in the mutual declaration containing this one

all :
• List of the names of the constructors for this inductive datatype.

ctors :
• 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
• An inductive type is called reflexive if it has at least one constructor that takes as an argument a function returning the same type we are defining. Consider the type:

inductive WideTree where
| branch: (Nat -> WideTree) -> WideTree
| leaf: WideTree


this is reflexive due to the presence of the branch : (Nat -> WideTree) -> WideTree constructor.

See also: 'Inductive Definitions in the system Coq Rules and Properties' by Christine Paulin-Mohring Section 2.2, Definition 3

isReflexive : Bool
• An inductive definition T is nested when there is a constructor with an argument x : F T, where F : Type → Type→ Type is some suitably behaved (ie strictly positive) function (Eg Array T, List T, 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.

Instances For
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 : ) (type : Lean.Expr) (numParams : Nat) (numIndices : Nat) (all : ) (ctors : ) (isRec : Bool) (isUnsafe : Bool) (isReflexive : Bool) (isNested : Bool) :
Equations
• One or more equations did not get rendered due to their size.
@[export lean_inductive_val_is_rec]
Equations
• = v.isRec
@[export lean_inductive_val_is_unsafe]
Equations
• = v.isUnsafe
@[export lean_inductive_val_is_reflexive]
Equations
• = v.isReflexive
@[export lean_inductive_val_is_nested]
Equations
• = v.isNested
Equations
structure Lean.ConstructorValextends :
• 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
Instances For
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 : ) (type : Lean.Expr) (induct : Lean.Name) (cidx : Nat) (numParams : Nat) (numFields : Nat) (isUnsafe : Bool) :
Equations
• One or more equations did not get rendered due to their size.
@[export lean_constructor_val_is_unsafe]
Equations
• = v.isUnsafe
• 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

Instances For
Equations
structure Lean.RecursorValextends :
• List of all inductive datatypes in the mutual declaration that generated this recursor

all :
• 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 :
• It supports K-like reduction. A recursor is said to support K-like reduction if one can assume it behaves like Eq under axiom K --- that is, it has one constructor, the constructor has 0 arguments, and it is an inductive predicate (ie, it lives in Prop).

Examples of inductives with K-like reduction is Eq, Acc, and And.intro. Non-examples are exists (where the constructor has arguments) and Or.intro (which has multiple constructors).

k : Bool
• isUnsafe : Bool
Instances For
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 : ) (type : Lean.Expr) (all : ) (numParams : Nat) (numIndices : Nat) (numMotives : Nat) (numMinors : Nat) (rules : ) (k : Bool) (isUnsafe : Bool) :
Equations
• One or more equations did not get rendered due to their size.
@[export lean_recursor_k]
Equations
@[export lean_recursor_is_unsafe]
Equations
• = v.isUnsafe
Equations
• = v.numParams + v.numMotives + v.numMinors + v.numIndices
Equations
• = v.numParams + v.numMotives + v.numMinors
Equations
• = v.numParams + v.numMotives
Equations
structure Lean.QuotValextends :
Instances For
Equations
@[export lean_mk_quot_val]
def Lean.mkQuotValEx (name : Lean.Name) (levelParams : ) (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]
Equations
• = v.kind
• axiomInfo:
• defnInfo:
• thmInfo:
• opaqueInfo:
• quotInfo:
• inductInfo:
• ctorInfo:
• recInfo:

Information associated with constant declarations.

Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• = ().levelParams
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x with | => true | => true | x => false
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x with | => true | x => false
Equations
• = match x with | => true | x => false

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.
Equations