funProp meta programming function 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 the convention is that coe is application of DFunLike.coe and this is assumed through out this file. It does not work with Lean's CoeFun.coe.

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 = ⇑(f a) b

the head of expression is considered to be f and not 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 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.getAppNumArgs (e : Lean.Expr) : ℕ

Counts the number n of arguments for an expression f a₁ .. aₙ where f can be bundled morphism.

Equations

• Mathlib.Meta.FunProp.Mor.getAppNumArgs e = Mathlib.Meta.FunProp.Mor.getAppNumArgs.go e 0

partial def Mathlib.Meta.FunProp.Mor.getAppNumArgs.go : Lean.Expr → ℕ → ℕ

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

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 = let nargs := Mathlib.Meta.FunProp.Mor.getAppNumArgs e; Mathlib.Meta.FunProp.Mor.withApp.go k e (mkArray nargs default) (nargs - 1)

def Mathlib.Meta.FunProp.Mor.withApp.go {α : Sort u_1} (k : Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → α) : Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → ℕ → α

def Mathlib.Meta.FunProp.Mor.getAppFn (e : Lean.Expr) : 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 = e

def Mathlib.Meta.FunProp.Mor.getAppArgs (e : Lean.Expr) : 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) => 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.

def Mathlib.Meta.FunProp.Mor.getArity (f : Lean.Expr) : Lean.MetaM ℕ

Get arity of morphism f. To get maximal arity of morphism f, this function tries to synthesize instance of FunLike as many times as possible.

Equations

• Mathlib.Meta.FunProp.Mor.getArity f = do let __do_lift ← Lean.Meta.inferType f Mathlib.Meta.FunProp.Mor.getTypeArityAux __do_lift 0

def Mathlib.Meta.FunProp.Mor.constArity (decl : Lean.Name) : Lean.MetaM ℕ

Arity of declared morphism with name decl.

Equations

• Mathlib.Meta.FunProp.Mor.constArity decl = do let info ← Lean.getConstInfo decl let __do_lift ← Mathlib.Meta.FunProp.Mor.getTypeArityAux (Lean.ConstantInfo.type info) 0 pure __do_lift

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

(fun x => e) a ==> e[x/a]

An example when coercions are involved: (fun x => ⇑((fun y => e) a)) b ==> e[y/a, x/b].

Equations

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

def Mathlib.Meta.FunProp.splitMorToCompOverArgs (e : Lean.Expr) (argIds : Array ℕ) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Split morphism function into composition by specifying over which arguments in the lambda body this split should be done.

Equations

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

def Mathlib.Meta.FunProp.splitMorToComp (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Split morphism function into composition by specifying over which arguments in the lambda body this split should be done.

Equations

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