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?

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

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

Is e morphism application?

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.Mor.isMorApp? e = pure none

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.

Equations

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

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

Equations

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

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

Morphism application

Equations

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

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.

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

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 (f.app 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 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 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.