Reducing Pi instances for indexing in the RefinedDiscrTree

@[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.

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

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

@[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).

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

def Lean.Meta.RefinedDiscrTree.reduceUnOpAux.distributeLambdas (lambdas : List FVarId) (type arg : Expr) : MetaM (Expr × Expr × List FVarId)

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

@[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).