Documentation

Lean.Elab.Tactic.BVDecide.Frontend.BVDecide.Reify

Reifies BitVec problems with boolean substructure.

source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of (x : 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.

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

Reify x, returns none if the reification procedure failed.

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

source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → Std.Tactic.BVDecide.BVUnOp) (shiftOpName congrThm : Name) :
LemmaM (Option ReifiedBVExpr)
source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.rotateReflection (distanceExpr innerExpr : Expr) (rotateOp : Nat → Std.Tactic.BVDecide.BVUnOp) (rotateOpName congrThm : Name) :
LemmaM (Option ReifiedBVExpr)
source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftConstReflection (β distanceExpr innerExpr : Expr) (shiftOp : Nat → Std.Tactic.BVDecide.BVUnOp) (shiftOpName congrThm : Name) :
LemmaM (Option ReifiedBVExpr)
source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftReflection (distanceExpr innerExpr : Expr) (shiftOp : {m n : Nat} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m) (shiftOpName congrThm : Name) :
LemmaM (Option ReifiedBVExpr)
source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.binaryReflection (lhsExpr rhsExpr : Expr) (op : Std.Tactic.BVDecide.BVBinOp) (congrThm : Name) :
LemmaM (Option ReifiedBVExpr)
source
def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.binaryCongrProof (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr congrThm : Expr) :
M (Option Expr)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.unaryReflection (innerExpr : Expr) (op : Std.Tactic.BVDecide.BVUnOp) (congrThm : Name) :
    LemmaM (Option ReifiedBVExpr)
    source
    def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.unaryCongrProof (inner : ReifiedBVExpr) (innerExpr congrProof : Expr) :
    M (Option Expr)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.goBvLit (x : Expr) :
      M (Option ReifiedBVExpr)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.of (t : 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.

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

        Reify t, returns none if the reification procedure failed.

        source
        partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred.of.binaryReflection (lhsExpr rhsExpr : Expr) (pred : Std.Tactic.BVDecide.BVBinPred) :
        LemmaM (Option ReifiedBVPred)
        source
        partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of (t : 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.

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

        Reify t, returns none if the reification procedure failed.

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

        source
        partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of.gateReflection (lhsExpr rhsExpr : Expr) (gate : Std.Tactic.BVDecide.Gate) :
        LemmaM (Option ReifiedBVLogical)
        source
        partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of.goPred (t : Expr) :
        LemmaM (Option ReifiedBVLogical)