inductive Lean.ReducibilityHints : Type

Reducibility hints guide the kernel's lazy delta reduction strategy. When the kernel encounters a definitional equality constraint

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

where f and g are definitions, it must decide which side to unfold. The rules (implemented in lazy_delta_reduction_step in src/kernel/type_checker.cpp) are:

• If f and g have the same hint kind:
  • Both .opaque or both .abbrev: unfold both.
  • Both .regular: unfold the one with the greater height first. If their heights are equal (in particular, if f and g are the same definition), first try to compare their arguments for definitional equality (short-circuiting the unfolding if they match), then unfold both.
• If f and g have different hint kinds: unfold the one that is not .opaque, preferring to unfold .abbrev over .regular.

The .regular constructor carries a UInt32 definitional height, which is computed by the elaborator as one plus the maximum height of all .regular constants appearing in the definition's body (see getMaxHeight). This means .abbrev and .opaque constants do not contribute to the height. When creating declarations via meta-programming, the height can be specified manually.

The hints only affect performance — they control the order in which definitions are unfolded, but never prevent the kernel from unfolding a definition during type checking.

The ReducibilityHints are not related to the @[reducible]/@[irreducible]/@[semireducible] attributes. Those attributes are used by the elaborator to control which definitions tactics like simp, rfl, and dsimp will unfold; they do not affect the kernel. Conversely, ReducibilityHints are set when a declaration is added to the kernel and cannot be changed afterwards.

• opaque : ReducibilityHints
• abbrev : ReducibilityHints
• regular : UInt32 → ReducibilityHints

def Lean.instInhabitedReducibilityHints.default : ReducibilityHints

@[implicit_reducible]

instance Lean.instInhabitedReducibilityHints : Inhabited ReducibilityHints

@[implicit_reducible]

instance Lean.instBEqReducibilityHints : BEq ReducibilityHints

def Lean.instBEqReducibilityHints.beq : ReducibilityHints → ReducibilityHints → Bool

@[export lean_mk_reducibility_hints_regular]

def Lean.mkReducibilityHintsRegularEx (h : UInt32) : ReducibilityHints

@[export lean_reducibility_hints_get_height]

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

def Lean.ReducibilityHints.lt : ReducibilityHints → ReducibilityHints → Bool

def Lean.ReducibilityHints.compare : ReducibilityHints → ReducibilityHints → Ordering

@[implicit_reducible]

instance Lean.ReducibilityHints.instOrd : Ord ReducibilityHints

def Lean.ReducibilityHints.isAbbrev : ReducibilityHints → Bool

def Lean.ReducibilityHints.isRegular : ReducibilityHints → Bool

structure Lean.ConstantVal : Type

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

• name : Name
• levelParams : List Name
• type : Expr

def Lean.instInhabitedConstantVal.default : ConstantVal

@[implicit_reducible]

instance Lean.instInhabitedConstantVal : Inhabited ConstantVal

@[implicit_reducible]

instance Lean.instBEqConstantVal : BEq ConstantVal

def Lean.instBEqConstantVal.beq : ConstantVal → ConstantVal → Bool

structure Lean.AxiomValextends Lean.ConstantVal : Type

• name : Name
• levelParams : List Name
• type : Expr
• isUnsafe : Bool

def Lean.instInhabitedAxiomVal.default : AxiomVal

@[implicit_reducible]

instance Lean.instInhabitedAxiomVal : Inhabited AxiomVal

@[implicit_reducible]

instance Lean.instBEqAxiomVal : BEq AxiomVal

def Lean.instBEqAxiomVal.beq : AxiomVal → AxiomVal → Bool

@[export lean_mk_axiom_val]

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

@[export lean_axiom_val_is_unsafe]

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

inductive Lean.DefinitionSafety : Type

• unsafe : DefinitionSafety
• safe : DefinitionSafety
• partial : DefinitionSafety

def Lean.instInhabitedDefinitionSafety.default : DefinitionSafety

@[implicit_reducible]

instance Lean.instInhabitedDefinitionSafety : Inhabited DefinitionSafety

@[implicit_reducible]

instance Lean.instBEqDefinitionSafety : BEq DefinitionSafety

def Lean.instBEqDefinitionSafety.beq : DefinitionSafety → DefinitionSafety → Bool

def Lean.instReprDefinitionSafety.repr : DefinitionSafety → Nat → Format

@[implicit_reducible]

instance Lean.instReprDefinitionSafety : Repr DefinitionSafety

structure Lean.DefinitionValextends Lean.ConstantVal : Type

• name : Name
• levelParams : List Name
• type : Expr
• value : Expr
• hints : ReducibilityHints
• safety : DefinitionSafety
• all : List Name

  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.

@[implicit_reducible]

instance Lean.instInhabitedDefinitionVal : Inhabited DefinitionVal

def Lean.instInhabitedDefinitionVal.default : DefinitionVal

def Lean.instBEqDefinitionVal.beq : DefinitionVal → DefinitionVal → Bool

@[implicit_reducible]

instance Lean.instBEqDefinitionVal : BEq DefinitionVal

@[export lean_mk_definition_val]

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

@[export lean_definition_val_get_safety]

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

structure Lean.TheoremValextends Lean.ConstantVal : Type

• name : Name
• levelParams : List Name
• type : Expr
• value : Expr
• all : List Name

  List of all (including this one) declarations in the same mutual block. See comment at DefinitionVal.all.

@[implicit_reducible]

instance Lean.instInhabitedTheoremVal : Inhabited TheoremVal

def Lean.instInhabitedTheoremVal.default : TheoremVal

def Lean.instBEqTheoremVal.beq : TheoremVal → TheoremVal → Bool

@[implicit_reducible]

instance Lean.instBEqTheoremVal : BEq TheoremVal

@[export lean_mk_theorem_val]

def Lean.mkTheoremValEx (name : Name) (levelParams : List Name) (type value : Expr) (all : List Name) : TheoremVal

structure Lean.OpaqueValextends Lean.ConstantVal : Type

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

• name : Name
• levelParams : List Name
• type : Expr
• value : Expr
• isUnsafe : Bool
• all : List Name

  List of all (including this one) declarations in the same mutual block. See comment at DefinitionVal.all.

def Lean.instInhabitedOpaqueVal.default : OpaqueVal

@[implicit_reducible]

instance Lean.instInhabitedOpaqueVal : Inhabited OpaqueVal

def Lean.instBEqOpaqueVal.beq : OpaqueVal → OpaqueVal → Bool

@[implicit_reducible]

instance Lean.instBEqOpaqueVal : BEq OpaqueVal

@[export lean_mk_opaque_val]

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

@[export lean_opaque_val_is_unsafe]

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

structure Lean.Constructor : Type

• name : Name
• type : Expr

def Lean.instInhabitedConstructor.default : Constructor

@[implicit_reducible]

instance Lean.instInhabitedConstructor : Inhabited Constructor

def Lean.instBEqConstructor.beq : Constructor → Constructor → Bool

@[implicit_reducible]

instance Lean.instBEqConstructor : BEq Constructor

structure Lean.InductiveType : Type

• name : Name
• type : Expr
• ctors : List Constructor

def Lean.instInhabitedInductiveType.default : InductiveType

@[implicit_reducible]

instance Lean.instInhabitedInductiveType : Inhabited InductiveType

@[implicit_reducible]

instance Lean.instBEqInductiveType : BEq InductiveType

def Lean.instBEqInductiveType.beq : InductiveType → InductiveType → Bool

inductive Lean.Declaration : Type

Declaration object that can be sent to the kernel.

• axiomDecl (val : AxiomVal) : Declaration
• defnDecl (val : DefinitionVal) : Declaration
• thmDecl (val : TheoremVal) : Declaration
• opaqueDecl (val : OpaqueVal) : Declaration
• quotDecl : Declaration
• mutualDefnDecl (defns : List DefinitionVal) : Declaration
• inductDecl (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) : Declaration

def Lean.instInhabitedDeclaration.default : Declaration

@[implicit_reducible]

instance Lean.instInhabitedDeclaration : Inhabited Declaration

def Lean.instBEqDeclaration.beq : Declaration → Declaration → Bool

@[implicit_reducible]

instance Lean.instBEqDeclaration : BEq Declaration

@[export lean_mk_inductive_decl]

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

@[export lean_is_unsafe_inductive_decl]

def Lean.Declaration.isUnsafeInductiveDeclEx : Declaration → Bool

def Lean.Declaration.definitionVal! : Declaration → DefinitionVal

def Lean.Declaration.getTopLevelNames : Declaration → List Name

Returns all top-level names to be defined by adding this declaration to the environment, i.e. excluding nested helper declarations generated automatically.

def Lean.Declaration.getNames : Declaration → List Name

Returns all names to be defined by adding this declaration to the environment. This does not include auxiliary definitions such as projections added by the elaborator, nor auxiliary recursors computed by the kernel for nested inductive types.

@[specialize #[]]

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

@[inline]

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

structure Lean.InductiveValextends Lean.ConstantVal : Type

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.

• name : Name
• levelParams : List Name
• type : Expr
• numParams : Nat

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

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

• numIndices : 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).

• all : List Name

  List of all (including this one) inductive datatypes in the mutual declaration containing this one

• ctors : List Name

  List of the names of the constructors for this inductive datatype.

• numNested : Nat

  Number of auxiliary data types produced from nested occurrences. 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, ...).

• isRec : Bool

  true when recursive (that is, the inductive type appears as an argument in a constructor).

• isUnsafe : Bool

  Whether the definition is flagged as unsafe.

• isReflexive : 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

@[implicit_reducible]

instance Lean.instInhabitedInductiveVal : Inhabited InductiveVal

def Lean.instInhabitedInductiveVal.default : InductiveVal

@[export lean_mk_inductive_val]

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

@[export lean_inductive_val_is_rec]

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

@[export lean_inductive_val_is_unsafe]

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

@[export lean_inductive_val_is_reflexive]

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

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

def Lean.InductiveVal.isNested (v : InductiveVal) : Bool

def Lean.InductiveVal.numTypeFormers (v : InductiveVal) : Nat

structure Lean.ConstructorValextends Lean.ConstantVal : Type

• name : Name
• levelParams : List Name
• type : Expr
• induct : Name

  Inductive type this constructor is a member of

• cidx : Nat

  Constructor index (i.e., Position in the inductive declaration)

• numParams : Nat

  Number of parameters in inductive datatype.

• numFields : Nat

  Number of fields (i.e., arity - nparams)

• isUnsafe : Bool

@[implicit_reducible]

instance Lean.instInhabitedConstructorVal : Inhabited ConstructorVal

def Lean.instInhabitedConstructorVal.default : ConstructorVal

def Lean.instBEqConstructorVal.beq : ConstructorVal → ConstructorVal → Bool

@[implicit_reducible]

instance Lean.instBEqConstructorVal : BEq ConstructorVal

@[export lean_mk_constructor_val]

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

@[export lean_constructor_val_is_unsafe]

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

structure Lean.RecursorRule : Type

Information for reducing a recursor

• ctor : Name

  Reduction rule for this Constructor

• nfields : Nat

  Number of fields (i.e., without counting inductive datatype parameters)

• rhs : Expr

  Right hand side of the reduction rule

def Lean.instInhabitedRecursorRule.default : RecursorRule

@[implicit_reducible]

instance Lean.instInhabitedRecursorRule : Inhabited RecursorRule

def Lean.instBEqRecursorRule.beq : RecursorRule → RecursorRule → Bool

@[implicit_reducible]

instance Lean.instBEqRecursorRule : BEq RecursorRule

structure Lean.RecursorValextends Lean.ConstantVal : Type

• name : Name
• levelParams : List Name
• type : Expr
• all : List Name

  List of all inductive datatypes in the mutual declaration that generated this recursor

• numParams : Nat

  Number of parameters

• numIndices : Nat

  Number of indices

• numMotives : Nat

  Number of motives

• numMinors : Nat

  Number of minor premises

• rules : List RecursorRule

  A reduction for each Constructor

• k : Bool

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

• isUnsafe : Bool

def Lean.instInhabitedRecursorVal.default : RecursorVal

@[implicit_reducible]

instance Lean.instInhabitedRecursorVal : Inhabited RecursorVal

def Lean.instBEqRecursorVal.beq : RecursorVal → RecursorVal → Bool

@[implicit_reducible]

instance Lean.instBEqRecursorVal : BEq RecursorVal

@[export lean_mk_recursor_val]

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

@[export lean_recursor_k]

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

@[export lean_recursor_is_unsafe]

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

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

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

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

def Lean.RecursorVal.getMajorInduct (v : RecursorVal) : Name

The inductive type of the major argument of the recursor.

inductive Lean.QuotKind : Type

• type : QuotKind
• ctor : QuotKind
• lift : QuotKind
• ind : QuotKind

@[implicit_reducible]

instance Lean.instInhabitedQuotKind : Inhabited QuotKind

def Lean.instInhabitedQuotKind.default : QuotKind

structure Lean.QuotValextends Lean.ConstantVal : Type

• name : Name
• levelParams : List Name
• type : Expr
• kind : QuotKind

@[implicit_reducible]

instance Lean.instInhabitedQuotVal : Inhabited QuotVal

def Lean.instInhabitedQuotVal.default : QuotVal

@[export lean_mk_quot_val]

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

@[export lean_quot_val_kind]

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

inductive Lean.ConstantInfo : Type

Information associated with constant declarations.

• axiomInfo (val : AxiomVal) : ConstantInfo
• defnInfo (val : DefinitionVal) : ConstantInfo
• thmInfo (val : TheoremVal) : ConstantInfo
• opaqueInfo (val : OpaqueVal) : ConstantInfo
• quotInfo (val : QuotVal) : ConstantInfo
• inductInfo (val : InductiveVal) : ConstantInfo
• ctorInfo (val : ConstructorVal) : ConstantInfo
• recInfo (val : RecursorVal) : ConstantInfo

def Lean.instInhabitedConstantInfo.default : ConstantInfo

@[implicit_reducible]

instance Lean.instInhabitedConstantInfo : Inhabited ConstantInfo

def Lean.ConstantInfo.toConstantVal : ConstantInfo → ConstantVal

def Lean.ConstantInfo.isUnsafe : ConstantInfo → Bool

def Lean.ConstantInfo.isPartial : ConstantInfo → Bool

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

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

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

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

def Lean.ConstantInfo.value? (info : ConstantInfo) (allowOpaque : Bool := false) : Option Expr

Returns the value of a definition. With allowOpaque := true, values of theorems and opaque declarations are also returned.

def Lean.ConstantInfo.hasValue (info : ConstantInfo) (allowOpaque : Bool := false) : Bool

Returns true if this declaration as a value for the purpose of reduction and type-checking, i.e. is a definition. With allowOpaque := true, theorems and opaque declarations are also considered to have values.

def Lean.ConstantInfo.value! (info : ConstantInfo) (allowOpaque : Bool := false) : Expr

Returns the value of a definition. With allowOpaque := true, values of theorems and opaque declarations are also returned.

def Lean.ConstantInfo.hints : ConstantInfo → ReducibilityHints

def Lean.ConstantInfo.isCtor : ConstantInfo → Bool

def Lean.ConstantInfo.isAxiom : ConstantInfo → Bool

def Lean.ConstantInfo.isInductive : ConstantInfo → Bool

def Lean.ConstantInfo.isDefinition : ConstantInfo → Bool

def Lean.ConstantInfo.isTheorem : ConstantInfo → Bool

def Lean.ConstantInfo.inductiveVal! : ConstantInfo → InductiveVal

def Lean.ConstantInfo.all : ConstantInfo → List Name

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

def Lean.mkRecName (declName : Name) : Name