Reifies BitVec problems with boolean substructure.

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of (x : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.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.ReifiedBVExpr.of.go (x : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

Reify x, returns none if the reification procedure failed.

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

Reify x or abstract it as an atom. Unless this function is called on something that is not a fixed-width BitVec it is always going to return some.

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftConstLikeReflection (distance : Nat) (innerExpr : Lean.Expr) (shiftOp : Nat → Std.Tactic.BVDecide.BVUnOp) (shiftOpName congrThm : Lean.Name) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.rotateReflection (distanceExpr innerExpr : Lean.Expr) (rotateOp : Nat → Std.Tactic.BVDecide.BVUnOp) (rotateOpName congrThm : Lean.Name) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftConstReflection (β distanceExpr innerExpr : Lean.Expr) (shiftOp : Nat → Std.Tactic.BVDecide.BVUnOp) (shiftOpName congrThm : Lean.Name) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftReflection (β distanceExpr innerExpr : Lean.Expr) (shiftOp : {m n : Nat} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m) (shiftOpName congrThm : Lean.Name) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.binaryReflection (lhsExpr rhsExpr : Lean.Expr) (op : Std.Tactic.BVDecide.BVBinOp) (congrThm : Lean.Name) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.binaryCongrProof (lhs rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (lhsExpr rhsExpr congrThm : 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.ReifiedBVExpr.of.unaryReflection (innerExpr : Lean.Expr) (op : Std.Tactic.BVDecide.BVUnOp) (congrThm : Lean.Name) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.unaryCongrProof (inner : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (innerExpr congrProof : 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.ReifiedBVExpr.of.goBvLit (x : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.M (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)

Equations

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

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.of (t : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.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.ReifiedBVPred.of.go (t : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred)

Reify t, returns none if the reification procedure failed.

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.of.binaryReflection (lhsExpr rhsExpr : Lean.Expr) (pred : Std.Tactic.BVDecide.BVBinPred) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred)

partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of (t : Lean.Expr) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.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.

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

Reify t, returns none if the reification procedure failed.

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

Reify t or abstract it as an atom. 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.gateReflection (lhsExpr rhsExpr : Lean.Expr) (gate : Std.Tactic.BVDecide.Gate) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical)

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