Provides the logic for reifying BitVec problems with boolean substructure.

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical : Type

A reified version of an Expr representing a BVLogicalExpr.

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = originalBVLogicalExpr.

• expr : Lean.Expr

  A cache for toExpr bvExpr

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkRefl (expr : Lean.Expr) : Lean.Expr

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkRefl expr = Lean.mkApp2 (Lean.mkConst `Eq.refl [1]) (Lean.mkConst `Bool) expr

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkTrans (x : Lean.Expr) (y : Lean.Expr) (z : Lean.Expr) (hxy : Lean.Expr) (hyz : Lean.Expr) : Lean.Expr

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkTrans x y z hxy hyz = Lean.mkApp6 (Lean.mkConst `Eq.trans [1]) (Lean.mkConst `Bool) x y z hxy hyz

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkEvalExpr (expr : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

Equations

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

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of (t : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of.gateReflection (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) (gate : Std.Tactic.BVDecide.Gate) (congrThm : Lake.Name) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical)

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of.goPred (t : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical)

Equations

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