1

我正在尝试在 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)

我该如何解决这个错误？

4

1 回答 1

2

出现此错误是因为raise它不是 F* 中的原语，但需要从中导入FStar.Exn（请参阅ulib/FStar.Exn.fst），它公开了此功能 -- raise。只需opening 这个模块就足够了。我还在下面修复了代码中的另一个小问题。

这是通过的代码版本：

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)

请注意，我还添加了requiresandensures子句。这是因为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)
于 2019-09-08T03:41:48.917 回答