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.

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.Forall {α : Sort u_1} (p : α → Sort u_2) : Sort (imax u_1 u_2)

An abbreviation of ∀ x, p x. It is used by fun_prop to represent Pi types as function applications and should not occur in any place other than the implementation of fun_prop.

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

Is name a coercion from some function space to functions?

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

Is e a coercion 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 → α → β

@[implicit_reducible]

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

def Mathlib.Meta.FunProp.Mor.instInhabitedArg.default : 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.

∀ x, p x is represented as Forall p.

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.