funProp data structure holding information about a function

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

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

funProp-normal form of a function is of the form fun x => f x₁ ... xₙ.

Throws and error if function can't be turned into funProp-normal form.

Examples: In funProp-normal form

fun x => f x
fun x => y + x

Not in funProp-normal form

fun x y => f x y
HAdd.hAdd y

Equations

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

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

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

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

Is f a constant function?

Equations

• Mathlib.Meta.FunProp.FunctionData.isConstantFun f = if (decide (Array.size f.mainArgs = 0) && !Lean.Expr.containsFVar f.fn (Lean.Expr.fvarId! f.mainVar)) = true then true else false

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

Domain type of f.

Equations

• Mathlib.Meta.FunProp.FunctionData.domainType f = 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 be put into funProp-normal form.

Equations

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

def Mathlib.Meta.FunProp.FunctionData.getCoeAppNumArgs? (f : Mathlib.Meta.FunProp.FunctionData) : Option ℕ

If f is in the form fun x => @DFunLike.coe F α β self f x₁ ... xₙ return the number of arguments of DFunLike.coe i.e. n + 5.

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 identity function.

Equations

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