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 functions?

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

Is e a coerction from some function space to functions?

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 App)

Is e morphism application?

partial def Mathlib.Meta.FunProp.Mor.whnfPred (e : Lean.Expr) (pred : Lean.Expr → Lean.MetaM Bool) : 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) : 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.

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 Arg

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

Morphism application

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

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

partial def Mathlib.Meta.FunProp.Mor.withApp.go {α : Type} (k : Lean.Expr → Array Arg → Lean.MetaM α) : Lean.Expr → Array 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.

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

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

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

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