Documentation

Mathlib.Tactic.FunProp.ToBatteries

funProp missing function from standard library #

source
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.
source
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
source
def Lean.Expr.swapBVars (e : Expr) (i j : Nat) :
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.
source
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.
source
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

source
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
source
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.
source
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.
source
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
source
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