funProp missing function from standard library

def Mathlib.Meta.FunProp.isOrderedSubsetOf {α : Type u_1} [Inhabited α] [DecidableEq α] (a : Array α) (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 : Nat) (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 : Nat) (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.