Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.ReifiedLemmas

Provides the logic for generating auxiliary lemmas during reification.

source
def Lean.Elab.Tactic.BVDecide.Frontend.addCondLemmas (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 bif discrExpr then lhsExpr else rhsExpr.
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Tactic.BVDecide.Frontend.addCondLemmas.mkCondTrueLemma (discr : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (atom lhs : 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.
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.addCondLemmas.mkCondFalseLemma (discr : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (atom 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.
      Instances For