funProp Meta programming functions like in Lean.Expr.* but for working with bundled morphisms.

Function application in normal lean expression looks like .app f x but when we work with bundled morphism f it looks like .app (.app coe f) x where f. In mathlib coe is usually DFunLike.coe but it can be any coercion that is registered with the coe attribute.

The main difference when working with expression involving morphisms is that the notion the head of expression changes. For example in:

  coe (f a) b

the head of expression is considered to be f and not coe.

def Mathlib.Meta.FunProp.Mor.isCoeFunName (name : Lean.Name) : Lean.CoreM Bool

Is name a coerction from some function space to functiosn?

Equations

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

def Mathlib.Meta.FunProp.Mor.isCoeFun (e : Lean.Expr) : Lean.MetaM Bool

Is e a coerction from some function space to functiosn?

Equations

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

structure Mathlib.Meta.FunProp.Mor.App : Type

Morphism application

• coe : Lean.Expr

  morphism coercion

• fn : Lean.Expr

  bundled morphism

• arg : Lean.Expr

  morphism argument

def Mathlib.Meta.FunProp.Mor.isMorApp? (e : Lean.Expr) : Lean.MetaM (Option Mathlib.Meta.FunProp.Mor.App)

Is e morphism application?

Equations

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

partial def Mathlib.Meta.FunProp.Mor.whnfPred (e : Lean.Expr) (pred : Lean.Expr → Lean.MetaM Bool) (cfg : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) : Lean.MetaM Lean.Expr

Weak normal head form of an expression involving morphism applications. Additionally, pred can specify which when to unfold definitions.

For example calling this on coe (f a) b will put f in weak normal head form instead of coe.

def Mathlib.Meta.FunProp.Mor.whnf (e : Lean.Expr) (cfg : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }) : Lean.MetaM Lean.Expr

Weak normal head form of an expression involving morphism applications.

For example calling this on coe (f a) b will put f in weak normal head form instead of coe.

Equations

• Mathlib.Meta.FunProp.Mor.whnf e cfg = Mathlib.Meta.FunProp.Mor.whnfPred e (fun (x : Lean.Expr) => pure false) cfg

structure Mathlib.Meta.FunProp.Mor.Arg : Type

Argument of morphism application that stores corresponding coercion if necessary

• expr : Lean.Expr

  argument of type α

• coe : Option Lean.Expr

  coercion F → α → β

instance Mathlib.Meta.FunProp.Mor.instInhabitedArg : Inhabited Mathlib.Meta.FunProp.Mor.Arg

Equations

• Mathlib.Meta.FunProp.Mor.instInhabitedArg = { default := { expr := default, coe := default } }

def Mathlib.Meta.FunProp.Mor.app (f : Lean.Expr) (arg : Mathlib.Meta.FunProp.Mor.Arg) : Lean.Expr

Morphism application

Equations

• Mathlib.Meta.FunProp.Mor.app f arg = match arg.coe with | none => Lean.Expr.app f arg.expr | some coe => Lean.Expr.app (Lean.Expr.app coe f) arg.expr

def Mathlib.Meta.FunProp.Mor.withApp {α : Type} (e : Lean.Expr) (k : Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → Lean.MetaM α) : Lean.MetaM α

Given e = f a₁ a₂ ... aₙ, returns k f #[a₁, ..., aₙ] where f can be bundled morphism.

Equations

• Mathlib.Meta.FunProp.Mor.withApp e k = Mathlib.Meta.FunProp.Mor.withApp.go k e #[]

partial def Mathlib.Meta.FunProp.Mor.withApp.go {α : Type} (k : Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → Lean.MetaM α) : Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → Lean.MetaM α

def Mathlib.Meta.FunProp.Mor.getAppFn (e : Lean.Expr) : Lean.MetaM Lean.Expr

If the given expression is a sequence of morphism applications f a₁ .. aₙ, return f. Otherwise return the input expression.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.Mor.getAppFn (Lean.Expr.mdata data b) = Mathlib.Meta.FunProp.Mor.getAppFn b
• Mathlib.Meta.FunProp.Mor.getAppFn (Lean.Expr.app f arg) = Mathlib.Meta.FunProp.Mor.getAppFn f
• Mathlib.Meta.FunProp.Mor.getAppFn e = pure e

def Mathlib.Meta.FunProp.Mor.getAppArgs (e : Lean.Expr) : Lean.MetaM (Array Mathlib.Meta.FunProp.Mor.Arg)

Given f a₁ a₂ ... aₙ, returns #[a₁, ..., aₙ] where f can be bundled morphism.

Equations

• Mathlib.Meta.FunProp.Mor.getAppArgs e = Mathlib.Meta.FunProp.Mor.withApp e fun (x : Lean.Expr) (xs : Array Mathlib.Meta.FunProp.Mor.Arg) => pure xs

def Mathlib.Meta.FunProp.Mor.mkAppN (f : Lean.Expr) (xs : Array Mathlib.Meta.FunProp.Mor.Arg) : Lean.Expr

mkAppN f #[a₀, ..., aₙ] ==> f a₀ a₁ .. aₙ where f can be bundled morphism.

Equations

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