小编Mat*_*ens的帖子

我看到很多使用 SBV 库的示例，如下所示：

f :: IO SatResult
f = sat $ do
      x <- sInteger "x"
      constraint $ x .< 200

对于接受 Haskell Int 的函数，我想在通过 Data.SBV 库传递给 Z3 的约束公式中使用该 Int：

f :: Int -> IO SatResult
f i = sat $ do
          x <- sInteger "x"
          constraint $ x .< (g i)
        where
          g = ???

如何从 Haskell Int 转换为 SInteger 或 OrdSymbolic 和 EqSymbolic 的一些适当实例以与 (.<) 和 (.==) 一起使用？

谢谢！