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 Mathlib.Meta.FunProp.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 : Mathlib.Meta.FunProp.FunctionData) : Lean.MetaM Lean.Expr

Turn function data back to expression.

Equations

• f.toExpr = Lean.Meta.withLCtx f.lctx f.insts (let body := Mathlib.Meta.FunProp.Mor.mkAppN f.fn f.args; Lean.Meta.mkLambdaFVars #[f.mainVar] body)

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

Is f an identity function?

Equations

• f.isIdentityFun = (decide (f.args.size = 0) && f.fn == f.mainVar)

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

Is f a constant function?

Equations

• f.isConstantFun = (decide (f.mainArgs.size = 0) && !f.fn.containsFVar f.mainVar.fvarId!)

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

Domain type of f.

Equations

• f.domainType = Lean.Meta.withLCtx f.lctx f.insts (Lean.Meta.inferType f.mainVar)

def Mathlib.Meta.FunProp.FunctionData.getFnConstName? (f : Mathlib.Meta.FunProp.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.

Equations

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

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

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

Equations

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

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: Lean.Expr → Mathlib.Meta.FunProp.MaybeFunctionData

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

• lam: Lean.Expr → Mathlib.Meta.FunProp.MaybeFunctionData

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

• data: Mathlib.Meta.FunProp.FunctionData → Mathlib.Meta.FunProp.MaybeFunctionData

  Function data has been successfully generated.

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

Turn MaybeFunctionData to the function.

Equations

• (Mathlib.Meta.FunProp.MaybeFunctionData.letE f).get = pure f
• (Mathlib.Meta.FunProp.MaybeFunctionData.lam f).get = pure f
• (Mathlib.Meta.FunProp.MaybeFunctionData.data d).get = d.toExpr

def Mathlib.Meta.FunProp.getFunctionData? (f : Lean.Expr) (unfoldPred : optParam (Lean.Name → Bool) fun (x : Lean.Name) => false) (cfg : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) : Lean.MetaM Mathlib.Meta.FunProp.MaybeFunctionData

Get FunctionData for f.

Equations

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

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

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

Equations

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

inductive Mathlib.Meta.FunProp.MorApplication : Type

Type of morphism application.

• underApplied: Mathlib.Meta.FunProp.MorApplication

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

• exact: Mathlib.Meta.FunProp.MorApplication

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

• overApplied: Mathlib.Meta.FunProp.MorApplication

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

• none: Mathlib.Meta.FunProp.MorApplication

  Not a morphism application.

instance Mathlib.Meta.FunProp.instInhabitedMorApplication : Inhabited Mathlib.Meta.FunProp.MorApplication

Equations

• Mathlib.Meta.FunProp.instInhabitedMorApplication = { default := Mathlib.Meta.FunProp.MorApplication.underApplied }

instance Mathlib.Meta.FunProp.instBEqMorApplication : BEq Mathlib.Meta.FunProp.MorApplication

Equations

• Mathlib.Meta.FunProp.instBEqMorApplication = { beq := Mathlib.Meta.FunProp.beqMorApplication✝ }

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

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

Equations

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

def Mathlib.Meta.FunProp.FunctionData.peeloffArgDecomposition (fData : Mathlib.Meta.FunProp.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

Equations

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

def Mathlib.Meta.FunProp.FunctionData.nontrivialDecomposition (fData : Mathlib.Meta.FunProp.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.

Equations

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

def Mathlib.Meta.FunProp.FunctionData.decompositionOverArgs (fData : Mathlib.Meta.FunProp.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.

Equations

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