funProp data structure holding information about a function

FunctionData holds data about function in the form fun x => f x₁ ... xₙ.

structure Mathlib.Meta.FunProp.FunctionData : Type

Structure storing parts of a function in funProp-normal form.

• lctx : Lean.LocalContext

  local context where mainVar exists

• insts : Lean.LocalInstances

  local instances

• fn : Lean.Expr

  main function

• args : Array Mor.Arg

  applied function arguments

• mainVar : Lean.Expr

  main variable

• mainArgs : Array ℕ

  indices of args that contain mainVars

def Mathlib.Meta.FunProp.FunctionData.toExpr (f : FunctionData) : Lean.MetaM Lean.Expr

Turn function data back to expression.

def Mathlib.Meta.FunProp.FunctionData.isIdentityFun (f : FunctionData) : Bool

Is f an identity function?

def Mathlib.Meta.FunProp.FunctionData.isConstantFun (f : FunctionData) : Bool

Is f a constant function?

def Mathlib.Meta.FunProp.FunctionData.domainType (f : FunctionData) : Lean.MetaM Lean.Expr

Domain type of f.

def Mathlib.Meta.FunProp.FunctionData.getFnConstName? (f : FunctionData) : Lean.MetaM (Option Lean.Name)

Is head function of f a constant?

If the head of f is a projection return the name of corresponding projection function.

def Mathlib.Meta.FunProp.getFunctionData (f : Lean.Expr) : Lean.MetaM FunctionData

Get FunctionData for f. Throws if f can't be put into funProp-normal form.

inductive Mathlib.Meta.FunProp.MaybeFunctionData : Type

Result of getFunctionData?. It returns function data if the function is in the form fun x => f y₁ ... yₙ. Two other cases are fun x => let y := ... or fun x y => ...

• letE (f : Lean.Expr) : MaybeFunctionData

  Can't generate function data as function body has let binder.

• lam (f : Lean.Expr) : MaybeFunctionData

  Can't generate function data as function body has lambda binder.

• data (fData : FunctionData) : MaybeFunctionData

  Function data has been successfully generated.

def Mathlib.Meta.FunProp.MaybeFunctionData.get (fData : MaybeFunctionData) : Lean.MetaM Lean.Expr

Turn MaybeFunctionData to the function.

def Mathlib.Meta.FunProp.getFunctionData? (f : Lean.Expr) (unfoldPred : Lean.Name → Bool := fun (x : Lean.Name) => false) : Lean.MetaM MaybeFunctionData

Get FunctionData for f.

def Mathlib.Meta.FunProp.FunctionData.unfoldHeadFVar? (fData : FunctionData) : Lean.MetaM (Option Lean.Expr)

If head function is a let-fvar unfold it and return resulting function. Return none otherwise.

inductive Mathlib.Meta.FunProp.MorApplication : Type

Type of morphism application.

• underApplied : MorApplication

  Of the form ⇑f i.e. missing argument.

• exact : MorApplication

  Of the form ⇑f x i.e. morphism and one argument is provided.

• overApplied : MorApplication

  Of the form ⇑f x y ... i.e. additional applied arguments y ....

• none : MorApplication

  Not a morphism application.

instance Mathlib.Meta.FunProp.instInhabitedMorApplication : Inhabited MorApplication

instance Mathlib.Meta.FunProp.instBEqMorApplication : BEq MorApplication

def Mathlib.Meta.FunProp.FunctionData.isMorApplication (f : FunctionData) : Lean.MetaM MorApplication

Is function body of f a morphism application? What kind?

def Mathlib.Meta.FunProp.FunctionData.peeloffArgDecomposition (fData : FunctionData) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Decomposes fun x => f y₁ ... yₙ into (fun g => g yₙ) ∘ (fun x y => f y₁ ... yₙ₋₁ y)

Returns none if:

• n=0
• yₙ contains x
• n=1 and (fun x y => f y) is identity function i.e. x=f

def Mathlib.Meta.FunProp.FunctionData.nontrivialDecomposition (fData : FunctionData) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Decompose function f = (← fData.toExpr) into composition of two functions.

Returns none if the decomposition would produce composition with identity function.

def Mathlib.Meta.FunProp.FunctionData.decompositionOverArgs (fData : FunctionData) (args : Array ℕ) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Decompose function fun x => f y₁ ... yₙ over specified argument indices #[i, j, ...].

The result is:

(fun (yᵢ',yⱼ',...) => f y₁ .. yᵢ' .. yⱼ' .. yₙ) ∘ (fun x => (yᵢ, yⱼ, ...))

This is not possible if yₗ for l ∉ #[i,j,...] still contains x. In such case none is returned.