Documentation

Mathlib.Lean.Meta.RefinedDiscrTree.Pi

Reducing Pi instances for indexing in the RefinedDiscrTree #

source
@[irreducible, specialize #[]]
def Lean.Meta.RefinedDiscrTree.etaExpand {α : Type} (args : Array Expr) (type : Expr) (lambdas : List FVarId) (goalArity : ℕ) (k : Array Expr → List FVarId → MetaM α) :
MetaM α

Introduce new lambdas by η-expansion.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.RefinedDiscrTree.reduceHBinOpAux (args : Array Expr) (lambdas : List FVarId) (instH instPi : Name) :
OptionT MetaM (Expr × Expr × Expr × List FVarId)

Normalize an application of a heterogeneous binary operator like HAdd.hAdd, using:

  • f = fun x => f x to increase the arity to 6
  • (f + g) a = f a + g a to decrease the arity to 6
  • (fun x => f x + g x) = f + g to get rid of any lambdas in front
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.RefinedDiscrTree.reduceHBinOpAux.distributeLambdas (lambdas : List FVarId) (type lhs rhs : Expr) :
MetaM (Expr × Expr × Expr × List FVarId)

use that (fun x => f x + g x) = f + g

Equations
source
@[inline]
def Lean.Meta.RefinedDiscrTree.reduceHBinOp (n : Name) (args : Array Expr) (lambdas : List FVarId) :
MetaM (Option (Expr × Expr × Expr × List FVarId))

Normalize an application if the head is +, *, - or /. Optionally return the (type, lhs, rhs, lambdas).

Equations
source
def Lean.Meta.RefinedDiscrTree.reduceUnOpAux (args : Array Expr) (lambdas : List FVarId) (instPi : Name) :
OptionT MetaM (Expr × Expr × List FVarId)

Normalize an application of a unary operator like Inv.inv, using:

  • f⁻¹ a = (f a)⁻¹ to decrease the arity to 3
  • (fun x => (f a)⁻¹) = f⁻¹ to get rid of any lambdas in front
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.RefinedDiscrTree.reduceUnOpAux.distributeLambdas (lambdas : List FVarId) (type arg : Expr) :
MetaM (Expr × Expr × List FVarId)

use that (fun x => (f x)⁻¹) = f⁻¹

Equations
source
@[inline]
def Lean.Meta.RefinedDiscrTree.reduceUnOp (n : Name) (args : Array Expr) (lambdas : List FVarId) :
MetaM (Option (Expr × Expr × List FVarId))

Normalize an application if the head is ⁻¹ or -. Optionally return the (type, arg, lambdas).

Equations