Documentation

Lean.Declaration

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

Instances For

instance Lean.instInhabitedReducibilityHints :

Inhabited ReducibilityHints

Equations

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

instance Lean.instBEqReducibilityHints :

BEq ReducibilityHints

Equations

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

@[export lean_mk_reducibility_hints_regular]

def Lean.mkReducibilityHintsRegularEx (h : UInt32) :

ReducibilityHints

Equations

Lean.mkReducibilityHintsRegularEx h = Lean.ReducibilityHints.regular h

@[export lean_reducibility_hints_get_height]

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

Equations

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

def Lean.ReducibilityHints.lt :

ReducibilityHints → 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

instance Lean.ReducibilityHints.instOrd :

Ord ReducibilityHints

Equations

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

def Lean.ReducibilityHints.isAbbrev :

ReducibilityHints → Bool

Equations

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

def Lean.ReducibilityHints.isRegular :

ReducibilityHints → Bool

Equations

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

structure Lean.ConstantVal :

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

name : Name
levelParams : List Name
type : Expr

Instances For

instance Lean.instInhabitedConstantVal :

Inhabited ConstantVal

Equations

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

instance Lean.instBEqConstantVal :

BEq ConstantVal

Equations

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

structure Lean.AxiomValextends Lean.ConstantVal :

Instances For

instance Lean.instInhabitedAxiomVal :

Inhabited AxiomVal

Equations

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

instance Lean.instBEqAxiomVal :

Equations

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

@[export lean_mk_axiom_val]

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

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 : AxiomVal) :

Equations

v.isUnsafeEx = v.isUnsafe

inductive Lean.DefinitionSafety :

Instances For

instance Lean.instInhabitedDefinitionSafety :

Inhabited DefinitionSafety

Equations

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

instance Lean.instBEqDefinitionSafety :

BEq DefinitionSafety

Equations

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

instance Lean.instReprDefinitionSafety :

Repr DefinitionSafety

Equations

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

structure Lean.DefinitionValextends Lean.ConstantVal :

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.

Instances For

instance Lean.instInhabitedDefinitionVal :

Inhabited DefinitionVal

Equations

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

instance Lean.instBEqDefinitionVal :

BEq DefinitionVal

Equations

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

@[export lean_mk_definition_val]

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

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 : DefinitionVal) :

DefinitionSafety

Equations

v.getSafetyEx = v.safety

structure Lean.TheoremValextends Lean.ConstantVal :

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.

Instances For

instance Lean.instInhabitedTheoremVal :

Inhabited TheoremVal

Equations

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

instance Lean.instBEqTheoremVal :

Equations

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

@[export lean_mk_theorem_val]

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

Equations

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

structure Lean.OpaqueValextends Lean.ConstantVal :

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.

Instances For

instance Lean.instInhabitedOpaqueVal :

Inhabited OpaqueVal

Equations

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

instance Lean.instBEqOpaqueVal :

Equations

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

@[export lean_mk_opaque_val]

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

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 : OpaqueVal) :

Equations

v.isUnsafeEx = v.isUnsafe

structure Lean.Constructor :

name : Name
type : Expr

Instances For

instance Lean.instInhabitedConstructor :

Inhabited Constructor

Equations

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

instance Lean.instBEqConstructor :

BEq Constructor

Equations

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

structure Lean.InductiveType :

name : Name
type : Expr
ctors : List Constructor

Instances For

instance Lean.instInhabitedInductiveType :

Inhabited InductiveType

Equations

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

instance Lean.instBEqInductiveType :

BEq InductiveType

Equations

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

inductive Lean.Declaration :

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

Instances For

instance Lean.instInhabitedDeclaration :

Inhabited Declaration

Equations

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

instance Lean.instBEqDeclaration :

BEq Declaration

Equations

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

@[export lean_mk_inductive_decl]

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

Equations

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

@[export lean_is_unsafe_inductive_decl]

def Lean.Declaration.isUnsafeInductiveDeclEx :

Declaration → Bool

Equations

(Lean.Declaration.inductDecl lparams nparams types isUnsafe).isUnsafeInductiveDeclEx = isUnsafe
x✝.isUnsafeInductiveDeclEx = false

def Lean.Declaration.definitionVal! :

Declaration → DefinitionVal

Equations

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

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.

Equations

(Lean.Declaration.axiomDecl val).getTopLevelNames = [val.name]
(Lean.Declaration.defnDecl val).getTopLevelNames = [val.name]
(Lean.Declaration.thmDecl val).getTopLevelNames = [val.name]
(Lean.Declaration.opaqueDecl val).getTopLevelNames = [val.name]
Lean.Declaration.quotDecl.getTopLevelNames = [`Quot]
(Lean.Declaration.mutualDefnDecl defns).getTopLevelNames = List.map (fun (x : Lean.DefinitionVal) => x.name) defns
(Lean.Declaration.inductDecl lparams nparams types isUnsafe).getTopLevelNames = List.map (fun (x : Lean.InductiveType) => x.name) types

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.

Equations

One or more equations did not get rendered due to their size.
(Lean.Declaration.axiomDecl val).getNames = [val.name]
(Lean.Declaration.defnDecl val).getNames = [val.name]
(Lean.Declaration.thmDecl val).getNames = [val.name]
(Lean.Declaration.opaqueDecl val).getNames = [val.name]
Lean.Declaration.quotDecl.getNames = [`Quot, `Quot.mk, `Quot.lift, `Quot.ind]
(Lean.Declaration.mutualDefnDecl defns).getNames = List.map (fun (x : Lean.DefinitionVal) => x.name) defns

@[specialize #[]]

def Lean.Declaration.foldExprM {α : Type} {m : Type → Type} [Monad m] (d : Declaration) (f : α → 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 : Declaration) (f : Expr → m Unit) :

Equations

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

structure Lean.InductiveValextends Lean.ConstantVal :

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

Instances For

Lean.instInhabitedInductiveVal

instance Lean.instInhabitedInductiveVal :

Inhabited InductiveVal

Equations

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

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

Equations

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

@[export lean_inductive_val_is_rec]

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

Equations

v.isRecEx = v.isRec

@[export lean_inductive_val_is_unsafe]

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

Equations

v.isUnsafeEx = v.isUnsafe

@[export lean_inductive_val_is_reflexive]

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

Equations

v.isReflexiveEx = v.isReflexive

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

Equations

v.numCtors = v.ctors.length

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

Equations

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

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

Equations

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

structure Lean.ConstructorValextends Lean.ConstantVal :

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

Instances For

instance Lean.instInhabitedConstructorVal :

Inhabited ConstructorVal

Equations

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

instance Lean.instBEqConstructorVal :

BEq ConstructorVal

Equations

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

@[export lean_mk_constructor_val]

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

Equations

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

@[export lean_constructor_val_is_unsafe]

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

Equations

v.isUnsafeEx = v.isUnsafe

structure Lean.RecursorRule :

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

Instances For

instance Lean.instInhabitedRecursorRule :

Inhabited RecursorRule

Equations

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

instance Lean.instBEqRecursorRule :

BEq RecursorRule

Equations

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

structure Lean.RecursorValextends Lean.ConstantVal :

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

Instances For

instance Lean.instInhabitedRecursorVal :

Inhabited RecursorVal

Equations

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

instance Lean.instBEqRecursorVal :

BEq RecursorVal

Equations

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

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

Equations

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

@[export lean_recursor_k]

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

Equations

v.kEx = v.k

@[export lean_recursor_is_unsafe]

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

Equations

v.isUnsafeEx = v.isUnsafe

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

Equations

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

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

Equations

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

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

Equations

v.getFirstMinorIdx = v.numParams + v.numMotives

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

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 → Expr → 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 : QuotKind
ctor : QuotKind
lift : QuotKind
ind : QuotKind

Instances For

Lean.instInhabitedQuotKind

instance Lean.instInhabitedQuotKind :

Inhabited QuotKind

Equations

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

structure Lean.QuotValextends Lean.ConstantVal :

Instances For

Lean.instInhabitedQuotVal

instance Lean.instInhabitedQuotVal :

Inhabited QuotVal

Equations

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

@[export lean_mk_quot_val]

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

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 : QuotVal) :

Equations

v.kindEx = v.kind

inductive Lean.ConstantInfo :

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

Instances For

Lean.instInhabitedConstantInfo

instance Lean.instInhabitedConstantInfo :

Inhabited ConstantInfo

Equations

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

def Lean.ConstantInfo.toConstantVal :

ConstantInfo → 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 :

ConstantInfo → Bool

Equations

def Lean.ConstantInfo.isPartial :

ConstantInfo → Bool

Equations

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

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

Equations

d.name = d.toConstantVal.name

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

Equations

d.levelParams = d.toConstantVal.levelParams

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

Equations

d.numLevelParams = d.levelParams.length

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

Equations

d.type = d.toConstantVal.type

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

Equations

One or more equations did not get rendered due to their size.
(Lean.ConstantInfo.thmInfo { name := name, levelParams := levelParams, type := type, value := value, all := all }).value? allowOpaque = some value
info.value? allowOpaque = none

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

Equations

(Lean.ConstantInfo.defnInfo val).hasValue allowOpaque = true
(Lean.ConstantInfo.thmInfo val).hasValue allowOpaque = true
(Lean.ConstantInfo.opaqueInfo val).hasValue allowOpaque = allowOpaque
info.hasValue allowOpaque = false

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

Equations

One or more equations did not get rendered due to their size.
(Lean.ConstantInfo.thmInfo { name := name, levelParams := levelParams, type := type, value := value, all := all }).value! allowOpaque = value
info.value! allowOpaque = panicWithPosWithDecl "Lean.Declaration" "Lean.ConstantInfo.value!" 485 31 "declaration with value expected"

def Lean.ConstantInfo.hints :

ConstantInfo → ReducibilityHints

Equations

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

def Lean.ConstantInfo.isCtor :

ConstantInfo → Bool

Equations

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

def Lean.ConstantInfo.isAxiom :

ConstantInfo → Bool

Equations

(Lean.ConstantInfo.axiomInfo val).isAxiom = true
x✝.isAxiom = false

def Lean.ConstantInfo.isInductive :

ConstantInfo → Bool

Equations

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

def Lean.ConstantInfo.isDefinition :

ConstantInfo → Bool

Equations

(Lean.ConstantInfo.defnInfo v).isDefinition = true
x✝.isDefinition = false

def Lean.ConstantInfo.isTheorem :

ConstantInfo → Bool

Equations

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

def Lean.ConstantInfo.inductiveVal! :

ConstantInfo → InductiveVal

Equations

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

def Lean.ConstantInfo.all :

ConstantInfo → List 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 : Name) :

Equations

Lean.mkRecName declName = declName.mkStr "rec"