funProp missing function from standard library

def Mathlib.Meta.FunProp.isOrderedSubsetOf {α : Type u_1} [Inhabited α] [DecidableEq α] (a b : Array α) : Bool

Check if a can be obtained by removing elements from b.

Equations

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

def Mathlib.Meta.FunProp.letTelescope {α : Type} {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] (e : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → n α) : n α

Telescope consuming only let bindings

Equations

• Mathlib.Meta.FunProp.letTelescope e k = Lean.Meta.map2MetaM (fun {α : Type} (k : Array Lean.Expr → Lean.Expr → Lean.MetaM α) => Mathlib.Meta.FunProp.letTelescopeImpl✝ e k) k

def Lean.Expr.swapBVars (e : Lean.Expr) (i j : Nat) : Lean.Expr

Swaps bvars indices i and j

NOTE: the indices i and j do not correspond to the n in bvar n. Rather they behave like indices in Expr.lowerLooseBVars, Expr.liftLooseBVars, etc.

TODO: This has to have a better implementation, but I'm still beyond confused with how bvar indices work

Equations

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

def Mathlib.Meta.FunProp.mkProdElem (xs : Array Lean.Expr) : Lean.MetaM Lean.Expr

For #[x₁, .., xₙ] create (x₁, .., xₙ).

Equations

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

def Mathlib.Meta.FunProp.mkProdProj (x : Lean.Expr) (i n : Nat) : Lean.MetaM Lean.Expr

For (x₀, .., xₙ₋₁) return xᵢ but as a product projection.

We need to know the total size of the product to be considered.

For example for xyz : X × Y × Z

• mkProdProj xyz 1 3 returns xyz.snd.fst.
• mkProdProj xyz 1 2 returns xyz.snd.

def Mathlib.Meta.FunProp.mkProdSplitElem (xs : Lean.Expr) (n : Nat) : Lean.MetaM (Array Lean.Expr)

For an element of a product type(of sizen) xs create an array of all possible projections i.e. #[xs.1, xs.2.1, xs.2.2.1, ..., xs.2..2]

Equations

• Mathlib.Meta.FunProp.mkProdSplitElem xs n = Array.mapM (fun (i : Nat) => Mathlib.Meta.FunProp.mkProdProj xs i n) (Array.range n)

def Mathlib.Meta.FunProp.mkUncurryFun (n : Nat) (f : Lean.Expr) : Lean.MetaM Lean.Expr

Uncurry function f in n arguments.

Equations

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

def Mathlib.Meta.FunProp.etaExpand1 (f : Lean.Expr) : Lean.MetaM Lean.Expr

Eta expand f in only one variable and reduce in others.

Examples:

  f                ==> fun x => f x
  fun x y => f x y ==> fun x => f x
  HAdd.hAdd y      ==> fun x => HAdd.hAdd y x
  HAdd.hAdd        ==> fun x => HAdd.hAdd x

Equations

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

def Mathlib.Meta.FunProp.betaThroughLet (f : Lean.Expr) (args : Array Lean.Expr) : Lean.Expr

Apply the given arguments to f, beta-reducing if f is a lambda expression. This variant does beta-reduction through let bindings without inlining them.

Example

beta' (fun x => let y := x * x; fun z => x + y + z) #[a,b]
==>
let y := a * a; a + y + b

Equations

• Mathlib.Meta.FunProp.betaThroughLet f args = Mathlib.Meta.FunProp.betaThroughLetAux✝ f args.toList

def Mathlib.Meta.FunProp.headBetaThroughLet (e : Lean.Expr) : Lean.Expr

Beta reduces head of an expression, (fun x => e) a ==> e[x/a]. This version applies arguments through let bindings without inlining them.

Example

headBeta' ((fun x => let y := x * x; fun z => x + y + z) a b)
==>
let y := a * a; a + y + b

Equations

• Mathlib.Meta.FunProp.headBetaThroughLet e = if Lean.Expr.isHeadBetaTargetFn true e.getAppFn = true then Mathlib.Meta.FunProp.betaThroughLet e.getAppFn e.getAppArgs else e