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.

Equations

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

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.

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

• 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 : 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

• Lean.Meta.RefinedDiscrTree.reduceHBinOp `HAdd.hAdd args lambdas = Lean.Meta.RefinedDiscrTree.reduceHBinOpAux args lambdas `instHAdd `Pi.instAdd
• Lean.Meta.RefinedDiscrTree.reduceHBinOp `HMul.hMul args lambdas = Lean.Meta.RefinedDiscrTree.reduceHBinOpAux args lambdas `instHMul `Pi.instMul
• Lean.Meta.RefinedDiscrTree.reduceHBinOp `HSub.hSub args lambdas = Lean.Meta.RefinedDiscrTree.reduceHBinOpAux args lambdas `instHSub `Pi.instSub
• Lean.Meta.RefinedDiscrTree.reduceHBinOp `HDiv.hDiv args lambdas = Lean.Meta.RefinedDiscrTree.reduceHBinOpAux args lambdas `instHDiv `Pi.instDiv
• Lean.Meta.RefinedDiscrTree.reduceHBinOp n args lambdas = pure none

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.

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

• 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 : 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

• 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