我正在尝试在 Simulink 模型的 Why3 规范中使用 32 位整数，并且我找到了mach.int 库，也就是说，至少在一个地方，它被描述为标准库的一部分。但是，当我尝试将它与以下导入命令一起使用时：
use import mach.int.Int32
我收到消息：
Library file not found: mach.int
这是我的第一个带有“。”的库。在其中，所以我不确定我的语法是否错误，或者这个库实际上不是标准库的一部分，或者我做错了什么。
mach.int.Int32使用模块的正确方法是什么？
附加细节
我的why3版本是 0.87.3：
▶ why3 --version
Why3 platform, version 0.87.3
我查看了我的 ~/.why3.conf 文件，发现了以下几行：
[main]
loadpath = "/opt/gps/share/why3/theories"
loadpath = "/opt/gps/share/why3/modules"
loadpath = "/opt/gps/share/spark/theories"
我查看/opt/gps/share/why3/modules(and /opt/gps/share/why3/theoriesand /opt/gps/share/spark/theories) 并发现 no mach.int.*，所以我在 中创建了一个mach.int.mlw文件/opt/gps/share/why3/modules，并确保它没why3问题：
▶ why3 prove -P z3 mach.int.mlw
mach.int.mlw Int WP_parameter infix / : Valid (0.01s)
mach.int.mlw Int WP_parameter infix % : Valid (0.01s)
mach.int.mlw Refint63 WP_parameter incr : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter decr : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix += : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix -= : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix *= : Valid (0.02s)
mach.int.mlw MinMax63 WP_parameter min : Valid (0.01s)
mach.int.mlw MinMax63 WP_parameter max : Valid (0.02s)
结果是一样的。