Reducing Pi instances for indexing in the RefinedDiscrTree

@[irreducible, specialize #[]]

def Lean.Meta.RefinedDiscrTree.etaExpand {α : Type} (args : Array Lean.Expr) (type : Lean.Expr) (lambdas : List Lean.FVarId) (goalArity : ℕ) (k : Array Lean.Expr → List Lean.FVarId → Lean.MetaM α) : Lean.MetaM α

Introduce new lambdas by η-expansion.

Equations

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

def Lean.Meta.RefinedDiscrTree.reduceHBinOpAux (args : Array Lean.Expr) (lambdas : List Lean.FVarId) (instH instPi : Lean.Name) : OptionT Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × List Lean.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.

def Lean.Meta.RefinedDiscrTree.reduceHBinOpAux.distributeLambdas (lambdas : List Lean.FVarId) (type lhs rhs : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr × List Lean.FVarId)

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.RefinedDiscrTree.reduceHBinOpAux.distributeLambdas [] type lhs rhs = pure (type, lhs, rhs, [])

@[inline]

def Lean.Meta.RefinedDiscrTree.reduceHBinOp (n : Lean.Name) (args : Array Lean.Expr) (lambdas : List Lean.FVarId) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × List Lean.FVarId))

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

def Lean.Meta.RefinedDiscrTree.reduceUnOpAux (args : Array Lean.Expr) (lambdas : List Lean.FVarId) (instPi : Lean.Name) : OptionT Lean.MetaM (Lean.Expr × Lean.Expr × List Lean.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.

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.RefinedDiscrTree.reduceUnOpAux.distributeLambdas [] type arg = pure (type, arg, [])

@[inline]

def Lean.Meta.RefinedDiscrTree.reduceUnOp (n : Lean.Name) (args : Array Lean.Expr) (lambdas : List Lean.FVarId) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × List Lean.FVarId))

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

Equations

• Lean.Meta.RefinedDiscrTree.reduceUnOp `Neg.neg args lambdas = Lean.Meta.RefinedDiscrTree.reduceUnOpAux args lambdas `Pi.instNeg
• Lean.Meta.RefinedDiscrTree.reduceUnOp `Inv.inv args lambdas = Lean.Meta.RefinedDiscrTree.reduceUnOpAux args lambdas `Pi.instInv
• Lean.Meta.RefinedDiscrTree.reduceUnOp n args lambdas = pure none