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

instance Lean.Meta.instBEqFunIndParamKind : BEq FunIndParamKind

instance Lean.Meta.instReprFunIndParamKind : Repr FunIndParamKind

instance Lean.Meta.instInhabitedFunIndParamKind : Inhabited FunIndParamKind

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

instance Lean.Meta.instInhabitedFunIndInfo : Inhabited FunIndInfo

instance Lean.Meta.instReprFunIndInfo : Repr FunIndInfo

opaque Lean.Meta.funIndInfoExt : MapDeclarationExtension FunIndInfo

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

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

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

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

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

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

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