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 : 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.

source
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.

source
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.

source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftConstLikeReflection (distance : Nat) (innerExpr : Lean.Expr) (shiftOp : Nat → Std.Tactic.BVDecide.BVUnOp) (shiftOpName : Lean.Name) (congrThm : Lean.Name) :
Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)
source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.rotateReflection (distanceExpr : Lean.Expr) (innerExpr : Lean.Expr) (rotateOp : Nat → Std.Tactic.BVDecide.BVUnOp) (rotateOpName : Lean.Name) (congrThm : Lean.Name) :
Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)
source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftConstReflection (β : Lean.Expr) (distanceExpr : Lean.Expr) (innerExpr : Lean.Expr) (shiftOp : Nat → Std.Tactic.BVDecide.BVUnOp) (shiftOpName : Lean.Name) (congrThm : Lean.Name) :
Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)
source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.shiftReflection (β : Lean.Expr) (distanceExpr : Lean.Expr) (innerExpr : Lean.Expr) (shiftOp : {m n : Nat} → Std.Tactic.BVDecide.BVExpr m → Std.Tactic.BVDecide.BVExpr n → Std.Tactic.BVDecide.BVExpr m) (shiftOpName : Lean.Name) (congrThm : Lean.Name) :
Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)
source
partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.binaryReflection (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) (op : Std.Tactic.BVDecide.BVBinOp) (congrThm : Lean.Name) :
Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)
source
def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.binaryCongrProof (lhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (rhs : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) (congrThm : Lean.Expr) :
Lean.Elab.Tactic.BVDecide.Frontend.M Lean.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 : Lean.Expr) (op : Std.Tactic.BVDecide.BVUnOp) (congrThm : Lean.Name) :
    Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr)
    source
    def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr.of.unaryCongrProof (inner : Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr) (innerExpr : Lean.Expr) (congrProof : Lean.Expr) :
    Lean.Elab.Tactic.BVDecide.Frontend.M Lean.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 : 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.
      Instances For
        source
        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.

        source
        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.

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

        source
        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.

        source
        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.

        source
        partial def Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical.of.gateReflection (lhsExpr : Lean.Expr) (rhsExpr : Lean.Expr) (gate : Std.Tactic.BVDecide.Gate) :
        Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (Option Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical)
        source
        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)