问题标签 [why3ml]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
why3 - Why3ML 中的布尔模式匹配
在其他 ML 变体（例如 SML）中，可以执行以下操作：
但是，使用 Why3ML 声明做类似的事情match会引发语法错误：
如何在元组中正确进行基于值的模式匹配？
formal-verification - 在Why3的谓词中调用我自己的函数
使用最新版本的 Why3 (1.0.0)，当我尝试执行以下操作时：
我收到以下形式的错误：文件“../something.why”，第 x 行，字符 yz：未绑定符号 'add_one'。难道我做错了什么？我看到的大多数WhyML 代码示例实际上仅使用内置/标准库函数，但确实调用了同一文件中定义的其他谓词。在定义谓词时，是否没有类似的方法来调用我在同一个文件中定义的函数？
sml - 在Why3ML 中输入 lambda 的正确方法是什么？
我想用 lambda 验证一个函数。例如：
但是，这会产生错误：
文件“map_reduce.mlw”，第 25 行，字符 4-7：此应用程序使用可变类型数组 int 实例化纯类型变量 'b
是否可以在Why3 中使用 lambda 函数？输入这些 lambda 函数的正确方法是什么？