Provides the logic for generating auxiliary lemmas during reification.

def Lean.Elab.Tactic.BVDecide.Frontend.addIfLemmas (discr : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (atom lhs rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (discrExpr atomExpr lhsExpr rhsExpr : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM Unit

This function adds the two lemmas:

• discrExpr = true → atomExpr = lhsExpr
• discrExpr = false → atomExpr = rhsExpr It assumes that discrExpr, lhsExpr and rhsExpr are the expressions corresponding to discr, lhs and rhs. Furthermore it assumes that atomExpr is of the form if discrExpr = true then lhsExpr else rhsExpr.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.addIfLemmas.mkIfTrueLemma (discr : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (atom lhs rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (discrExpr atomExpr lhsExpr rhsExpr : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical)

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.addIfLemmas.mkIfFalseLemma (discr : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (atom lhs rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (discrExpr atomExpr lhsExpr rhsExpr : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical)

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.addIfLemmas.mkIfLemma (discrVal : Bool) (discr : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (atom lhs rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (discrExpr atomExpr lhsExpr rhsExpr : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical)

Equations

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