This module defines the data structure and environment extension to remember how to map the function's arguments to the functional induction principle's arguments. Also used for functional cases.

inductive Lean.Meta.FunIndParamKind : Type

• dropped : FunIndParamKind
• param : FunIndParamKind
• target : FunIndParamKind

@[implicit_reducible]

instance Lean.Meta.instBEqFunIndParamKind : BEq FunIndParamKind

Equations

• Lean.Meta.instBEqFunIndParamKind = { beq := Lean.Meta.instBEqFunIndParamKind.beq }

def Lean.Meta.instBEqFunIndParamKind.beq : FunIndParamKind → FunIndParamKind → Bool

Equations

• Lean.Meta.instBEqFunIndParamKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.Meta.instReprFunIndParamKind : Repr FunIndParamKind

Equations

• Lean.Meta.instReprFunIndParamKind = { reprPrec := Lean.Meta.instReprFunIndParamKind.repr }

def Lean.Meta.instReprFunIndParamKind.repr : FunIndParamKind → Nat → Format

Equations

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

@[implicit_reducible]

instance Lean.Meta.instInhabitedFunIndParamKind : Inhabited FunIndParamKind

Equations

• Lean.Meta.instInhabitedFunIndParamKind = { default := Lean.Meta.instInhabitedFunIndParamKind.default }

structure Lean.Meta.FunIndInfo : Type

A FunIndInfo indicates how a function's arguments map to the arguments of the functional induction (resp. cases) theorem.

The size of params also indicates the arity of the function.

• funName : Name
• funIndName : Name
• levelMask : Array Bool

  true means that the corresponding level parameter of the function is also a level param of the induction principle.

• params : Array FunIndParamKind

@[implicit_reducible]

instance Lean.Meta.instInhabitedFunIndInfo : Inhabited FunIndInfo

Equations

• Lean.Meta.instInhabitedFunIndInfo = { default := Lean.Meta.instInhabitedFunIndInfo.default }

def Lean.Meta.instReprFunIndInfo.repr : FunIndInfo → Nat → Format

Equations

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

@[implicit_reducible]

instance Lean.Meta.instReprFunIndInfo : Repr FunIndInfo

Equations

• Lean.Meta.instReprFunIndInfo = { reprPrec := Lean.Meta.instReprFunIndInfo.repr }

opaque Lean.Meta.funIndInfoExt : MapDeclarationExtension FunIndInfo

def Lean.Meta.getFunInductName (declName : Name) (unfolding : Bool := false) : Name

Equations

• Lean.Meta.getFunInductName declName unfolding = if unfolding = true then declName ++ `induct_unfolding else declName ++ `induct

def Lean.Meta.getFunCasesName (declName : Name) (unfolding : Bool := false) : Name

Equations

• Lean.Meta.getFunCasesName declName unfolding = if unfolding = true then declName ++ `fun_cases_unfolding else declName ++ `fun_cases

def Lean.Meta.getMutualInductName (declName : Name) (unfolding : Bool := false) : Name

Equations

• Lean.Meta.getMutualInductName declName unfolding = if unfolding = true then declName ++ `mutual_induct_unfolding else declName ++ `mutual_induct

def Lean.Meta.getFunInduct? (unfolding cases : Bool) (declName : Name) : CoreM (Option Name)

Equations

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

def Lean.Meta.setFunIndInfo (funIndInfo : FunIndInfo) : CoreM Unit

Equations

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

def Lean.Meta.getFunIndInfoForInduct? (inductName : Name) : CoreM (Option FunIndInfo)

Equations

• Lean.Meta.getFunIndInfoForInduct? inductName = do let __do_lift ← Lean.getEnv pure (Lean.Meta.funIndInfoExt.find? __do_lift inductName)

def Lean.Meta.getFunIndInfo? (cases unfolding : Bool) (funName : Name) : CoreM (Option FunIndInfo)

Equations

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