问在Why3ML中键入lambda的正确方法是什么？
EN

Stack Overflow用户

提问于 2019-01-23 18:02:22

回答 1查看 97关注 0票数 1

我想用lambda验证一个函数。例如：

  let map (t : array int) (f : array int -> array int) : array int =
    f t

但是，这会产生一个错误：

文件"map_reduce.mlw"，第25行，字符4-7:此应用程序使用可变类型数组int实例化纯类型变量'b‘。

在Why3中可以使用lambda函数吗？键入这些lambda函数的正确方法是什么？

发布于 2020-05-08 14:08:13

Why3中的Lambda函数是纯函数。特别是，它们的类型不能包含任何可变区域。这就是你的定义被拒绝的原因。将array替换为没有区域的类型(例如，set )，效果很好：

use set.Set
let map (t : set int) (f : set int -> set int) : set int = f t

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/54333137

复制

相似问题

问在Why3ML中键入lambda的正确方法是什么？EN