Lean.Declaration

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

source

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

Bool

Equations

Lean.AxiomVal.isUnsafeEx v = v.isUnsafe

source

inductive Lean.DefinitionSafety :

Type

source

instance Lean.instReprDefinitionSafety :

Repr Lean.DefinitionSafety

Equations

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

source

instance Lean.instBEqDefinitionSafety :

BEq Lean.DefinitionSafety

Equations

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

source

instance Lean.instInhabitedDefinitionSafety :

Inhabited Lean.DefinitionSafety

Equations

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

source

structure Lean.DefinitionVal extends Lean.ConstantVal :

Type

source

instance Lean.instInhabitedDefinitionVal :

Inhabited Lean.DefinitionVal

Equations

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

source

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

Lean.DefinitionVal

Equations

Lean.mkDefinitionValEx name levelParams type val hints safety = { toConstantVal := { name := name, levelParams := levelParams, type := type }, value := val, hints := hints, safety := safety }

source

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

Lean.DefinitionSafety

Equations

Lean.DefinitionVal.getSafetyEx v = v.safety

source

structure Lean.TheoremVal extends Lean.ConstantVal :

Type

value : Lean.Expr

source

instance Lean.instInhabitedTheoremVal :

Inhabited Lean.TheoremVal

Equations

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

source

structure Lean.OpaqueVal extends Lean.ConstantVal :

Type

value : Lean.Expr
isUnsafe : Bool

source

instance Lean.instInhabitedOpaqueVal :

Inhabited Lean.OpaqueVal

Equations

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

source

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

Lean.OpaqueVal

Equations

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

source

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

Bool

Equations

Lean.OpaqueVal.isUnsafeEx v = v.isUnsafe

source

structure Lean.Constructor :

Type

name : Lean.Name
type : Lean.Expr

source

instance Lean.instInhabitedConstructor :

Inhabited Lean.Constructor

Equations

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

source

structure Lean.InductiveType :

Type

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

source

instance Lean.instInhabitedInductiveType :

Inhabited Lean.InductiveType

Equations

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

source

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

source

instance Lean.instInhabitedDeclaration :

Inhabited Lean.Declaration

Equations

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

source

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

source

def Lean.Declaration.isUnsafeInductiveDeclEx :

Lean.Declaration → Bool

Equations

Lean.Declaration.isUnsafeInductiveDeclEx x = match x with | Lean.Declaration.inductDecl x x_1 x_2 isUnsafe => isUnsafe | x => false

source

@[specialize]

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

m α

Equations

Lean.Declaration.foldExprM d f a = match d with | Lean.Declaration.quotDecl => pure a | Lean.Declaration.axiomDecl { toConstantVal := { name := x, levelParams := x_1, type := type }, isUnsafe := x_2 } => f a type | Lean.Declaration.defnDecl { toConstantVal := { name := x, levelParams := x_1, type := type }, value := value, hints := x_2, safety := x_3 } => do let a ← f a type f a value | Lean.Declaration.opaqueDecl { toConstantVal := { name := x, levelParams := x_1, type := type }, value := value, isUnsafe := x_2 } => do let a ← f a type f a value | Lean.Declaration.thmDecl { toConstantVal := { name := x, levelParams := x_1, type := type }, value := value } => do let a ← f a type f a value | Lean.Declaration.mutualDefnDecl vals => List.foldlM (fun a v => do let a ← f a v.toConstantVal.type f a v.value) a vals | Lean.Declaration.inductDecl x x_1 inductTypes x_2 => List.foldlM (fun a inductType => do let a ← f a inductType.type List.foldlM (fun a ctor => f a ctor.type) a inductType.ctors) a inductTypes

source

@[inline]

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

m Unit

Equations

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

source

structure Lean.InductiveVal extends Lean.ConstantVal :

Type

numParams : Nat
numIndices : Nat
all : List Lean.Name
ctors : List Lean.Name
isRec : Bool
isUnsafe : Bool
isReflexive : Bool
isNested : Bool

source

instance Lean.instInhabitedInductiveVal :

Inhabited Lean.InductiveVal

Equations

Lean.instInhabitedInductiveVal = { default := { toConstantVal := default, numParams := default, numIndices := default, all := default, ctors := default, isRec := default, isUnsafe := default, isReflexive := default, isNested := default } }

source

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

Lean.mkInductiveValEx name levelParams type numParams numIndices all ctors isRec isUnsafe isReflexive isNested = { toConstantVal := { name := name, levelParams := levelParams, type := type }, numParams := numParams, numIndices := numIndices, all := all, ctors := ctors, isRec := isRec, isUnsafe := isUnsafe, isReflexive := isReflexive, isNested := isNested }

source

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

Bool

Equations

Lean.InductiveVal.isRecEx v = v.isRec

source

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

Bool

Equations

Lean.InductiveVal.isUnsafeEx v = v.isUnsafe

source

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

Bool

Equations

Lean.InductiveVal.isReflexiveEx v = v.isReflexive

source

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

Bool

Equations

Lean.InductiveVal.isNestedEx v = v.isNested

source

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

Nat

Equations

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

source

structure Lean.ConstructorVal extends Lean.ConstantVal :

Type

induct : Lean.Name
cidx : Nat
numParams : Nat
numFields : Nat
isUnsafe : Bool

source

instance Lean.instInhabitedConstructorVal :

Inhabited Lean.ConstructorVal

Equations

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

source

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

Lean.mkConstructorValEx name levelParams type induct cidx numParams numFields isUnsafe = { toConstantVal := { name := name, levelParams := levelParams, type := type }, induct := induct, cidx := cidx, numParams := numParams, numFields := numFields, isUnsafe := isUnsafe }

source

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

Bool

Equations

Lean.ConstructorVal.isUnsafeEx v = v.isUnsafe

source

structure Lean.RecursorRule :

Type

ctor : Lean.Name
nfields : Nat
rhs : Lean.Expr

source

instance Lean.instInhabitedRecursorRule :

Inhabited Lean.RecursorRule

Equations

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

source

structure Lean.RecursorVal extends Lean.ConstantVal :

Type

all : List Lean.Name
numParams : Nat
numIndices : Nat
numMotives : Nat
numMinors : Nat
rules : List Lean.RecursorRule
k : Bool
isUnsafe : Bool

source

instance Lean.instInhabitedRecursorVal :

Inhabited Lean.RecursorVal

Equations

Lean.instInhabitedRecursorVal = { default := { toConstantVal := default, all := default, numParams := default, numIndices := default, numMotives := default, numMinors := default, rules := default, k := default, isUnsafe := default } }

source

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

Lean.mkRecursorValEx name levelParams type all numParams numIndices numMotives numMinors rules k isUnsafe = { toConstantVal := { name := name, levelParams := levelParams, type := type }, all := all, numParams := numParams, numIndices := numIndices, numMotives := numMotives, numMinors := numMinors, rules := rules, k := k, isUnsafe := isUnsafe }

source

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

Bool

Equations

Lean.RecursorVal.kEx v = v.k

source

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

Bool

Equations

Lean.RecursorVal.isUnsafeEx v = v.isUnsafe

source

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

Nat

Equations

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

source

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

Nat

Equations

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

source

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

Nat

Equations

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

source

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

Lean.Name

Equations

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

source

inductive Lean.QuotKind :

Type

source

instance Lean.instInhabitedQuotKind :

Inhabited Lean.QuotKind

Equations

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

source

structure Lean.QuotVal extends Lean.ConstantVal :

Type

kind : Lean.QuotKind

source

instance Lean.instInhabitedQuotVal :

Inhabited Lean.QuotVal

Equations

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

source

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 = { toConstantVal := { name := name, levelParams := levelParams, type := type }, kind := kind }

source

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

Lean.QuotKind

Equations

Lean.QuotVal.kindEx v = v.kind

source

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

source

instance Lean.instInhabitedConstantInfo :

Inhabited Lean.ConstantInfo

Equations

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

source

def Lean.ConstantInfo.toConstantVal :

Lean.ConstantInfo → Lean.ConstantVal

Equations

Lean.ConstantInfo.toConstantVal x = match x with | Lean.ConstantInfo.defnInfo { toConstantVal := d, value := x, hints := x_1, safety := x_2 } => d | Lean.ConstantInfo.axiomInfo { toConstantVal := d, isUnsafe := x } => d | Lean.ConstantInfo.thmInfo { toConstantVal := d, value := x } => d | Lean.ConstantInfo.opaqueInfo { toConstantVal := d, value := x, isUnsafe := x_1 } => d | Lean.ConstantInfo.quotInfo { toConstantVal := d, kind := x } => d | Lean.ConstantInfo.inductInfo { toConstantVal := d, numParams := x, numIndices := x_1, all := x_2, ctors := x_3, isRec := x_4, isUnsafe := x_5, isReflexive := x_6, isNested := x_7 } => d | Lean.ConstantInfo.ctorInfo { toConstantVal := d, induct := x, cidx := x_1, numParams := x_2, numFields := x_3, isUnsafe := x_4 } => d | Lean.ConstantInfo.recInfo { toConstantVal := d, all := x, numParams := x_1, numIndices := x_2, numMotives := x_3, numMinors := x_4, rules := x_5, k := x_6, isUnsafe := x_7 } => d

source

def Lean.ConstantInfo.isUnsafe :

Lean.ConstantInfo → Bool

Equations

Lean.ConstantInfo.isUnsafe x = match x with | Lean.ConstantInfo.defnInfo v => v.safety == Lean.DefinitionSafety.unsafe | Lean.ConstantInfo.axiomInfo v => v.isUnsafe | Lean.ConstantInfo.thmInfo v => false | Lean.ConstantInfo.opaqueInfo v => v.isUnsafe | Lean.ConstantInfo.quotInfo v => false | Lean.ConstantInfo.inductInfo v => v.isUnsafe | Lean.ConstantInfo.ctorInfo v => v.isUnsafe | Lean.ConstantInfo.recInfo v => v.isUnsafe

source

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

Lean.Name

Equations

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

source

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

List Lean.Name

Equations

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

source

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

Nat

Equations

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

source

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

Lean.Expr

Equations

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

source

def Lean.ConstantInfo.value? :

Lean.ConstantInfo → Option Lean.Expr

Equations

Lean.ConstantInfo.value? x = match x with | Lean.ConstantInfo.defnInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, value := r, hints := x_3, safety := x_4 } => some r | Lean.ConstantInfo.thmInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, value := r } => some r | x => none

source

def Lean.ConstantInfo.hasValue :

Lean.ConstantInfo → Bool

Equations

Lean.ConstantInfo.hasValue x = match x with | Lean.ConstantInfo.defnInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, value := r, hints := x_3, safety := x_4 } => true | Lean.ConstantInfo.thmInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, value := r } => true | x => false

source

def Lean.ConstantInfo.value! :

Lean.ConstantInfo → Lean.Expr

Equations

Lean.ConstantInfo.value! x = match x with | Lean.ConstantInfo.defnInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, value := r, hints := x_3, safety := x_4 } => r | Lean.ConstantInfo.thmInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, value := r } => r | x => panicWithPosWithDecl "Lean.Declaration" "Lean.ConstantInfo.value!" 367 33 "declaration with value expected"

source

def Lean.ConstantInfo.hints :

Lean.ConstantInfo → Lean.ReducibilityHints

Equations

Lean.ConstantInfo.hints x = match x with | Lean.ConstantInfo.defnInfo { toConstantVal := { name := x, levelParams := x_1, type := x_2 }, value := x_3, hints := r, safety := x_4 } => r | x => Lean.ReducibilityHints.opaque