F*在匹配体中引发异常
F*在匹配体中引发异常
提问于 2019-09-08 02:10:27
我试图在F*中创建一个函数来确定列表的最小元素，如果列表是空的，我想抛出一个异常。到目前为止，我掌握的代码如下：
module MinList
exception EmptyList
val min_list: list int -> Exn int
let rec min_list l = match l with
| [] -> raise EmptyList
| single_el :: [] -> single_el
| hd :: tl -> min hd (min_list tl)但是，当我试图验证该文件时，会得到以下错误：
mcve.fst(7,10-7,15): (Error 72) Identifier not found: [raise]
1 error was reported (see above)如何纠正此错误？
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-09-08 03:41:48
出现此错误是因为raise不是F*中的原语，而是需要从FStar.Exn (参见ulib/FStar.Exn.fst)导入，后者公开了这个函数-- raise。简单地说，对这个模块进行open就足够了。在代码中还有一个小问题，我在下面也做了修正。
下面是通过的代码的版本：
module MinList
open FStar.Exn
exception EmptyList
val min_list: list int -> Exn int (requires True) (ensures (fun _ -> True))
let rec min_list l = match l with
| [] -> raise EmptyList
| single_el :: [] -> single_el
| hd :: tl -> min hd (min_list tl)注意，我还添加了requires和ensures子句。这是因为Exn效应要求这些子句对其中的代码进行推理。但是，如果用例恰好有上述子句(即true和true)，那么您可以使用方便的同义词Ex (参见ulib/FStar.Pervasives.fst)。因此，下面的代码也是有效的，并且行为与上面的代码完全相同。
module MinList
open FStar.Exn
exception EmptyList
val min_list: list int -> Ex int
let rec min_list l = match l with
| [] -> raise EmptyList
| single_el :: [] -> single_el
| hd :: tl -> min hd (min_list tl)页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/57838693
复制相关文章
相似问题
腾讯云开发者
