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

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

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

@[implicit_reducible]

instance Lean.Meta.instReprFunIndParamKind : Repr FunIndParamKind

@[implicit_reducible]

instance Lean.Meta.instInhabitedFunIndParamKind : Inhabited FunIndParamKind

def Lean.Meta.instInhabitedFunIndParamKind.default : 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

def Lean.Meta.instInhabitedFunIndInfo.default : FunIndInfo

@[implicit_reducible]

instance Lean.Meta.instInhabitedFunIndInfo : Inhabited FunIndInfo

@[implicit_reducible]

instance Lean.Meta.instReprFunIndInfo : Repr FunIndInfo

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

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)