inductive Lean.ReducibilityHints : Type

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.

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

instance Lean.instInhabitedReducibilityHints : Inhabited Lean.ReducibilityHints

Equations

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

instance Lean.instBEqReducibilityHints : BEq Lean.ReducibilityHints

Equations

• Lean.instBEqReducibilityHints = { beq := Lean.beqReducibilityHints✝ }

@[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) : UInt32

Equations

• (Lean.ReducibilityHints.regular h_2).getHeightEx = h_2
• h.getHeightEx = 0

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

Equations

• Lean.ReducibilityHints.abbrev.lt Lean.ReducibilityHints.abbrev = false
• Lean.ReducibilityHints.abbrev.lt x = true
• (Lean.ReducibilityHints.regular d₁).lt (Lean.ReducibilityHints.regular d₂) = decide (d₁ > d₂)
• (Lean.ReducibilityHints.regular a).lt Lean.ReducibilityHints.opaque = true
• x✝.lt x = false

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

Equations

• Lean.ReducibilityHints.abbrev.compare Lean.ReducibilityHints.abbrev = Ordering.eq
• Lean.ReducibilityHints.abbrev.compare x = Ordering.lt
• (Lean.ReducibilityHints.regular a).compare Lean.ReducibilityHints.abbrev = Ordering.gt
• (Lean.ReducibilityHints.regular d₁).compare (Lean.ReducibilityHints.regular d₂) = compare d₂ d₁
• (Lean.ReducibilityHints.regular a).compare Lean.ReducibilityHints.opaque = Ordering.lt
• Lean.ReducibilityHints.opaque.compare Lean.ReducibilityHints.opaque = Ordering.eq
• Lean.ReducibilityHints.opaque.compare x = Ordering.gt

instance Lean.ReducibilityHints.instOrd : Ord Lean.ReducibilityHints

Equations

• Lean.ReducibilityHints.instOrd = { compare := Lean.ReducibilityHints.compare }

def Lean.ReducibilityHints.isAbbrev : Lean.ReducibilityHints → Bool

Equations

• Lean.ReducibilityHints.abbrev.isAbbrev = true
• x.isAbbrev = false

def Lean.ReducibilityHints.isRegular : Lean.ReducibilityHints → Bool

Equations

• (Lean.ReducibilityHints.regular h_1).isRegular = true
• x.isRegular = false

structure Lean.ConstantVal : Type

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

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

instance Lean.instInhabitedConstantVal : Inhabited Lean.ConstantVal

Equations

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

instance Lean.instBEqConstantVal : BEq Lean.ConstantVal

Equations

• Lean.instBEqConstantVal = { beq := Lean.beqConstantVal✝ }

structure Lean.AxiomValextends Lean.ConstantVal : Type

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

instance Lean.instInhabitedAxiomVal : Inhabited Lean.AxiomVal

Equations

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

instance Lean.instBEqAxiomVal : BEq Lean.AxiomVal

Equations

• Lean.instBEqAxiomVal = { beq := Lean.beqAxiomVal✝ }

@[export lean_mk_axiom_val]

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

Equations

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

@[export lean_axiom_val_is_unsafe]

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

Equations

• v.isUnsafeEx = v.isUnsafe

inductive Lean.DefinitionSafety : Type

• unsafe: Lean.DefinitionSafety
• safe: Lean.DefinitionSafety
• partial: Lean.DefinitionSafety

instance Lean.instInhabitedDefinitionSafety : Inhabited Lean.DefinitionSafety

Equations

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

instance Lean.instBEqDefinitionSafety : BEq Lean.DefinitionSafety

Equations

• Lean.instBEqDefinitionSafety = { beq := Lean.beqDefinitionSafety✝ }

instance Lean.instReprDefinitionSafety : Repr Lean.DefinitionSafety

Equations

• Lean.instReprDefinitionSafety = { reprPrec := Lean.reprDefinitionSafety✝ }

structure Lean.DefinitionValextends Lean.ConstantVal : Type

• name : Lean.Name
• levelParams : List Lean.Name
• type : Lean.Expr
• value : Lean.Expr
• hints : Lean.ReducibilityHints
• safety : Lean.DefinitionSafety
• all : List Lean.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.

instance Lean.instInhabitedDefinitionVal : Inhabited Lean.DefinitionVal

Equations

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

instance Lean.instBEqDefinitionVal : BEq Lean.DefinitionVal

Equations

• Lean.instBEqDefinitionVal = { beq := Lean.beqDefinitionVal✝ }

@[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

• Lean.mkDefinitionValEx name levelParams type value hints safety all = { name := name, levelParams := levelParams, type := type, value := value, hints := hints, safety := safety, all := all }

@[export lean_definition_val_get_safety]

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

Equations

• v.getSafetyEx = v.safety

structure Lean.TheoremValextends Lean.ConstantVal : Type

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

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

instance Lean.instInhabitedTheoremVal : Inhabited Lean.TheoremVal

Equations

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

instance Lean.instBEqTheoremVal : BEq Lean.TheoremVal

Equations

• Lean.instBEqTheoremVal = { beq := Lean.beqTheoremVal✝ }

@[export lean_mk_theorem_val]

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

Equations

• Lean.mkTheoremValEx name levelParams type value all = { name := name, levelParams := levelParams, type := type, value := value, all := all }

structure Lean.OpaqueValextends Lean.ConstantVal : Type

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

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

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

instance Lean.instInhabitedOpaqueVal : Inhabited Lean.OpaqueVal

Equations

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

instance Lean.instBEqOpaqueVal : BEq Lean.OpaqueVal

Equations

• Lean.instBEqOpaqueVal = { beq := Lean.beqOpaqueVal✝ }

@[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) : Lean.OpaqueVal

Equations

• Lean.mkOpaqueValEx name levelParams type value isUnsafe all = { 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) : Bool

Equations

• v.isUnsafeEx = 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 } }

instance Lean.instBEqConstructor : BEq Lean.Constructor

Equations

• Lean.instBEqConstructor = { beq := Lean.beqConstructor✝ }

structure Lean.InductiveType : Type

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

instance Lean.instInhabitedInductiveType : Inhabited Lean.InductiveType

Equations

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

instance Lean.instBEqInductiveType : BEq Lean.InductiveType

Equations

• Lean.instBEqInductiveType = { beq := Lean.beqInductiveType✝ }

inductive Lean.Declaration : Type

Declaration object that can be sent to the kernel.

• 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

instance Lean.instInhabitedDeclaration : Inhabited Lean.Declaration

Equations

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

instance Lean.instBEqDeclaration : BEq Lean.Declaration

Equations

• Lean.instBEqDeclaration = { beq := Lean.beqDeclaration✝ }

@[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.inductDecl lparams nparams types isUnsafe).isUnsafeInductiveDeclEx = isUnsafe
• x.isUnsafeInductiveDeclEx = false

def Lean.Declaration.definitionVal! : Lean.Declaration → Lean.DefinitionVal

Equations

• (Lean.Declaration.defnDecl val).definitionVal! = val
• x.definitionVal! = panicWithPosWithDecl "Lean.Declaration" "Lean.Declaration.definitionVal!" 194 9 "Expected a `Declaration.defnDecl`."

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Declaration.quotDecl.foldExprM f a = pure a
• (Lean.Declaration.axiomDecl { name := name, levelParams := levelParams, type := type, isUnsafe := isUnsafe }).foldExprM f a = f a type
• (Lean.Declaration.thmDecl { name := name, levelParams := levelParams, type := type, value := value, all := all }).foldExprM f a = do let a ← f a type f a value
• (Lean.Declaration.mutualDefnDecl vals).foldExprM f a = List.foldlM (fun (a : α) (v : Lean.DefinitionVal) => do let a ← f a v.type f a v.value) a vals

@[inline]

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

Equations

• d.forExprM f = d.foldExprM (fun (x : Unit) (a : Lean.Expr) => f a) ()

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 : Lean.Name
• levelParams : List Lean.Name
• type : Lean.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 Lean.Name

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

• ctors : List Lean.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

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) (numNested : Nat) (isRec : Bool) (isUnsafe : Bool) (isReflexive : 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) : Bool

Equations

• v.isRecEx = v.isRec

@[export lean_inductive_val_is_unsafe]

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

Equations

• v.isUnsafeEx = v.isUnsafe

@[export lean_inductive_val_is_reflexive]

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

Equations

• v.isReflexiveEx = v.isReflexive

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

Equations

• v.numCtors = v.ctors.length

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

Equations

• v.isNested = decide (v.numNested > 0)

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

Equations

• v.numTypeFormers = v.all.length + v.numNested

structure Lean.ConstructorValextends Lean.ConstantVal : Type

• name : Lean.Name
• levelParams : List Lean.Name
• type : Lean.Expr
• induct : Lean.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

instance Lean.instInhabitedConstructorVal : Inhabited Lean.ConstructorVal

Equations

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

instance Lean.instBEqConstructorVal : BEq Lean.ConstructorVal

Equations

• Lean.instBEqConstructorVal = { beq := Lean.beqConstructorVal✝ }

@[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) : Bool

Equations

• v.isUnsafeEx = v.isUnsafe

structure Lean.RecursorRule : Type

Information for reducing a recursor

• ctor : Lean.Name

  Reduction rule for this Constructor

• nfields : Nat

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

• rhs : Lean.Expr

  Right hand side of the reduction rule

instance Lean.instInhabitedRecursorRule : Inhabited Lean.RecursorRule

Equations

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

instance Lean.instBEqRecursorRule : BEq Lean.RecursorRule

Equations

• Lean.instBEqRecursorRule = { beq := Lean.beqRecursorRule✝ }

structure Lean.RecursorValextends Lean.ConstantVal : Type

• name : Lean.Name
• levelParams : List Lean.Name
• type : Lean.Expr
• all : List Lean.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 Lean.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

instance Lean.instInhabitedRecursorVal : Inhabited Lean.RecursorVal

Equations

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

instance Lean.instBEqRecursorVal : BEq Lean.RecursorVal

Equations

• Lean.instBEqRecursorVal = { beq := Lean.beqRecursorVal✝ }

@[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) : Bool

Equations

• v.kEx = v.k

@[export lean_recursor_is_unsafe]

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

Equations

• v.isUnsafeEx = v.isUnsafe

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

Equations

• v.getMajorIdx = v.numParams + v.numMotives + v.numMinors + v.numIndices

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

Equations

• v.getFirstIndexIdx = v.numParams + v.numMotives + v.numMinors

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

Equations

• v.getFirstMinorIdx = v.numParams + v.numMotives

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

The inductive type of the major argument of the recursor.

Equations

• v.getMajorInduct = Lean.RecursorVal.getMajorInduct.go v.getMajorIdx v.type

def Lean.RecursorVal.getMajorInduct.go : Nat → Lean.Expr → Lean.Name

Equations

• Lean.RecursorVal.getMajorInduct.go 0 x = x.bindingDomain!.getAppFn.constName!
• Lean.RecursorVal.getMajorInduct.go n.succ x = Lean.RecursorVal.getMajorInduct.go n x.bindingBody!

inductive Lean.QuotKind : Type

• type: Lean.QuotKind
• ctor: Lean.QuotKind
• lift: Lean.QuotKind
• ind: Lean.QuotKind

instance Lean.instInhabitedQuotKind : Inhabited Lean.QuotKind

Equations

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

structure Lean.QuotValextends Lean.ConstantVal : Type

• name : Lean.Name
• levelParams : List Lean.Name
• type : Lean.Expr
• 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) : Lean.QuotVal

Equations

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

@[export lean_quot_val_kind]

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

Equations

• v.kindEx = v.kind

inductive Lean.ConstantInfo : Type

Information associated with constant declarations.

• 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

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.
• (Lean.ConstantInfo.defnInfo { toConstantVal := d, value := value, hints := hints, safety := safety, all := all }).toConstantVal = d
• (Lean.ConstantInfo.axiomInfo { toConstantVal := d, isUnsafe := isUnsafe }).toConstantVal = d
• (Lean.ConstantInfo.thmInfo { toConstantVal := d, value := value, all := all }).toConstantVal = d
• (Lean.ConstantInfo.opaqueInfo { toConstantVal := d, value := value, isUnsafe := isUnsafe, all := all }).toConstantVal = d
• (Lean.ConstantInfo.quotInfo { toConstantVal := d, kind := kind }).toConstantVal = d
• (Lean.ConstantInfo.ctorInfo { toConstantVal := d, induct := induct, cidx := cidx, numParams := numParams, numFields := numFields, isUnsafe := isUnsafe }).toConstantVal = d

def Lean.ConstantInfo.isUnsafe : Lean.ConstantInfo → Bool

Equations

• (Lean.ConstantInfo.defnInfo v).isUnsafe = (v.safety == Lean.DefinitionSafety.unsafe)
• (Lean.ConstantInfo.axiomInfo v).isUnsafe = v.isUnsafe
• (Lean.ConstantInfo.thmInfo val).isUnsafe = false
• (Lean.ConstantInfo.opaqueInfo v).isUnsafe = v.isUnsafe
• (Lean.ConstantInfo.quotInfo val).isUnsafe = false
• (Lean.ConstantInfo.inductInfo v).isUnsafe = v.isUnsafe
• (Lean.ConstantInfo.ctorInfo v).isUnsafe = v.isUnsafe
• (Lean.ConstantInfo.recInfo v).isUnsafe = v.isUnsafe

def Lean.ConstantInfo.isPartial : Lean.ConstantInfo → Bool

Equations

• (Lean.ConstantInfo.defnInfo v).isPartial = (v.safety == Lean.DefinitionSafety.partial)
• x.isPartial = false

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

Equations

• d.name = d.toConstantVal.name

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

Equations

• d.levelParams = d.toConstantVal.levelParams

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

Equations

• d.numLevelParams = d.levelParams.length

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

Equations

• d.type = d.toConstantVal.type

def Lean.ConstantInfo.value? : Lean.ConstantInfo → Option Lean.Expr

Equations

• (Lean.ConstantInfo.defnInfo { name := name, levelParams := levelParams, type := type, value := r, hints := hints, safety := safety, all := all }).value? = some r
• (Lean.ConstantInfo.thmInfo { name := name, levelParams := levelParams, type := type, value := r, all := all }).value? = some r
• x.value? = none

def Lean.ConstantInfo.hasValue : Lean.ConstantInfo → Bool

Equations

• (Lean.ConstantInfo.defnInfo val).hasValue = true
• (Lean.ConstantInfo.thmInfo val).hasValue = true
• x.hasValue = false

def Lean.ConstantInfo.value! : Lean.ConstantInfo → Lean.Expr

Equations

• (Lean.ConstantInfo.defnInfo { name := name, levelParams := levelParams, type := type, value := r, hints := hints, safety := safety, all := all }).value! = r
• (Lean.ConstantInfo.thmInfo { name := name, levelParams := levelParams, type := type, value := r, all := all }).value! = r
• x.value! = panicWithPosWithDecl "Lean.Declaration" "Lean.ConstantInfo.value!" 461 33 "declaration with value expected"

def Lean.ConstantInfo.hints : Lean.ConstantInfo → Lean.ReducibilityHints

Equations

• (Lean.ConstantInfo.defnInfo { name := name, levelParams := levelParams, type := type, value := value, hints := r, safety := safety, all := all }).hints = r
• x.hints = Lean.ReducibilityHints.opaque

def Lean.ConstantInfo.isCtor : Lean.ConstantInfo → Bool

Equations

• (Lean.ConstantInfo.ctorInfo val).isCtor = true
• x.isCtor = false

def Lean.ConstantInfo.isInductive : Lean.ConstantInfo → Bool

Equations

• (Lean.ConstantInfo.inductInfo val).isInductive = true
• x.isInductive = false

def Lean.ConstantInfo.isTheorem : Lean.ConstantInfo → Bool

Equations

• (Lean.ConstantInfo.thmInfo val).isTheorem = true
• x.isTheorem = false

def Lean.ConstantInfo.inductiveVal! : Lean.ConstantInfo → Lean.InductiveVal

Equations

• (Lean.ConstantInfo.inductInfo val).inductiveVal! = val
• x.inductiveVal! = panicWithPosWithDecl "Lean.Declaration" "Lean.ConstantInfo.inductiveVal!" 481 9 "Expected a `ConstantInfo.inductInfo`."

def Lean.ConstantInfo.all : Lean.ConstantInfo → List Lean.Name

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

Equations

• (Lean.ConstantInfo.inductInfo val).all = val.all
• (Lean.ConstantInfo.defnInfo val).all = val.all
• (Lean.ConstantInfo.thmInfo val).all = val.all
• (Lean.ConstantInfo.opaqueInfo val).all = val.all
• x.all = [x.name]

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

Equations

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