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.

Equations

• Mathlib.Meta.FunProp.Forall p = ((x : α) → p x)

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

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

def Mathlib.Meta.FunProp.Mor.instInhabitedArg.default : Arg

Equations

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

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

Equations

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

∀ x, p x is represented as Forall p.

Equations

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

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.