def Blaster.Optimize.optimizeProjection? (n : Lean.Name) (idx : Nat) (s : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Given a projection a.i apply the following normalization rules:

• When projectCore? a i := some re
  • return some re
• Otherwise
  • When a := Blaster.dite' c (fun h : c => t₁) (fun h : ¬ c => t₂)
    • return some Blaster.dite' c (fun h : c => t₁.i ) (fun h : ¬ c => t₂.i)
  • when a := match₁ e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁ ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ
    • return some match₁ e₁, ..., eₙ with | p₍₁₎₍₁₎, ..., p₍₁₎₍ₙ₎ => t₁.i ... | p₍ₘ₎₍₁₎, ..., p₍ₘ₎₍ₙ₎ => tₘ.i

Equations

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

def Blaster.Optimize.optimizeProjection?.updateDIteExprWithProj (typeName : Lean.Name) (idx : Nat) (ite_cond ite_e : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Blaster.Optimize.optimizeProjection?.updateDIteExprWithProj typeName idx ite_cond (Lean.Expr.lam n t body bi) = pure (Lean.Expr.lam n t (Lean.mkProj typeName idx body) bi)

def Blaster.Optimize.optimizeProjection?.diteProj? (n : Lean.Name) (s : Lean.Expr) (typeName : Lean.Name) (idx : Nat) (struct : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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

def Blaster.Optimize.optimizeProjection?.updateRhsWithProj (typeName : Lean.Name) (idx : Nat) (lhs : Array Lean.Expr) (rhs : Lean.Expr) : TranslateEnvT Lean.Expr

Equations

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

def Blaster.Optimize.optimizeProjection?.matchProj? (n : Lean.Name) (s : Lean.Expr) (typeName : Lean.Name) (idx : Nat) (struct : Lean.Expr) : TranslateEnvT (Option Lean.Expr)

Equations

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