F* Raising Exception in match body

Question

I am trying to create a function in F* to determine the minimum element of a list, and I want to throw an exception if the list is empty. The code I have so far is below:

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)

When I try to verify the file, however, I get the following error:

mcve.fst(7,10-7,15): (Error 72) Identifier not found: [raise]
1 error was reported (see above)

How can I fix this error?

Answer 1

This error comes up because raise is not a primitive in F* but needs to be imported from FStar.Exn (see ulib/FStar.Exn.fst), which exposes this function -- raise. Simply opening this module should be sufficient. There is one more minor issue in the code that I have also fixed below.

Here's the version of the code that goes through:

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)

Notice that I also have added requires and ensures clauses. This is because the Exn effect expects a these clauses to reason about the code in it. If your use case however, has exactly the above clauses (i.e., true and true), then you can use the convenient synonym for this, Ex (see ulib/FStar.Pervasives.fst). Thus, the following code is also valid and will behave exactly the same as the above code.

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)