Documentation

Lean.Meta.Tactic.BVDecide.Reflect.ReifiedBVExpr

Provides the logic for reifying BitVec expressions.

source
def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.mkEvalExpr (w : Nat) (expr : Expr) :
M Expr

Build BVExpr.eval atoms expr where atoms is the assignment stored in the monad.

Instances For
    source
    def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.mkBVRefl (w : Nat) (expr : Expr) :
    Expr
    Instances For
      source
      def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.mkAtom (e : Expr) (width : Nat) (synthetic : Bool) :
      M ReifiedBVExpr

      Register e as an atom of width that might potentially be synthetic.

      Instances For
        source
        def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.getNatOrBvValue? (ty expr : Expr) :
        M (Option Nat)

        Parse expr as a Nat or BitVec constant depending on ty.

        Instances For
          source
          def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.bitVecAtom (x : Expr) (synthetic : Bool) :
          M (Option ReifiedBVExpr)

          Construct an uninterpreted BitVec atom from x, potentially synthetic.

          Instances For
            source
            def Lean.Meta.Tactic.BVDecide.ReifiedBVExpr.mkBVConst {w : Nat} (val : BitVec w) :
            M ReifiedBVExpr

            Build a reified version of the constant val.

            Instances For