Reifies BitVec problems with boolean substructure.

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of (origExpr : Expr) : LemmaM (Option ReifiedBVExpr)

Reify an Expr that's a constant-width BitVec. Unless this function is called on something that is not a constant-width BitVec it is always going to return some.

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.of (origExpr : Expr) : LemmaM (Option ReifiedBVPred)

Reify an Expr that is a predicate about BitVec. Unless this function is called on something that is not a Bool it is always going to return some.

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of (origExpr : Expr) : LemmaM (Option ReifiedBVLogical)

Reify an Expr that is a boolean expression containing predicates about BitVec as atoms. Unless this function is called on something that is not a Bool it is always going to return some.