Provides the logic for generating auxiliary lemmas during reification.

def Lean.Elab.Tactic.BVDecide.Frontend.addCondLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr) (discrExpr atomExpr lhsExpr rhsExpr : Expr) : 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 bif discrExpr then lhsExpr else rhsExpr.

Equations

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