Provides the logic for reifying BitVec problems with boolean substructure.

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.

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.ofPred (bvPred : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical

Construct a ReifiedBVLogical from ReifiedBVPred by wrapping it as an atom.

Equations

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

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

Construct an uninterrpeted Bool atom from t.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkBoolConst (val : Bool) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical

Build a reified version of the constant val.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate (lhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) (gate : Std.Tactic.BVDecide.Gate) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical

Construct the reified version of applying the gate in gate to lhs and rhs. This function assumes that lhsExpr and rhsExpr are the corresponding expressions to lhs and rhs.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate.congrThmOfGate (gate : Std.Tactic.BVDecide.Gate) : Lean.Name

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate.congrThmOfGate Std.Tactic.BVDecide.Gate.and = `Std.Tactic.BVDecide.Reflect.Bool.and_congr
• Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate.congrThmOfGate Std.Tactic.BVDecide.Gate.xor = `Std.Tactic.BVDecide.Reflect.Bool.xor_congr
• Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate.congrThmOfGate Std.Tactic.BVDecide.Gate.beq = `Std.Tactic.BVDecide.Reflect.Bool.beq_congr
• Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkGate.congrThmOfGate Std.Tactic.BVDecide.Gate.imp = `Std.Tactic.BVDecide.Reflect.Bool.imp_congr

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkNot (sub : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (subExpr : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical

Construct the reified version of Bool.not subExpr. This function assumes that subExpr is the expression corresponding to sub.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.mkIte (discr : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (lhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical) (discrExpr : Lean.Expr) (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical

Construct the reified version of if discrExpr then lhsExpr else rhsExpr. This function assumes that discrExpr, lhsExprandrhsExprare the corresponding expressions to `discr, lhsandrhs`.

Equations

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