why3 - 需要帮助定义机器整数

Question

我在规范中使用该mach.int库（另请参阅此问题），并且我正在尝试定义一个类型为的常量int32：

let constant_out1: int32 = 1 in
…

但是，在分析时，why3 返回消息：

This term has type int, but is expected to have type int32

我注意到Bounded_int（Int32用 type 实例化int32）有以下内容：

  val of_int (n:int) : t
    requires { "expl:integer overflow" in_bounds n }
    ensures  { to_int result = n }

但是，我似乎无法使用它来投射1到int32. 例如，如果我使用：

let constant_out1: int32 = Int32.of_int(1) in
…

我得到消息unbound symbol 'Int32.of_int'。我已经尝试了很多这样的排列，但都没有成功。谁能提供指导，告诉我为什么我想1成为那种类型的人int32？