Lemmas validating the normalization and simplifications rules on Prop

theorem Blaster.Blaster.and_left {a b : Prop} (h : a ∧ b) : a

theorem Blaster.Blaster.and_right {a b : Prop} (h : a ∧ b) : b

def Blaster.mkBlasterAndLeft : Optimize.TranslateEnvT Lean.Expr

Return Blaster.and_left const expression and cache result.

Equations

• Blaster.mkBlasterAndLeft = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.Blaster.and_left)

def Blaster.mkBlasterAndRight : Optimize.TranslateEnvT Lean.Expr

Return Blaster.and_right const expression and cache result.

Equations

• Blaster.mkBlasterAndRight = Blaster.Optimize.mkExpr (Lean.mkConst `Blaster.Blaster.and_right)