test/coq/pass/throw_fact.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

default Order dec
$include <prelude.sail>

union exception = {
  BadInput : int
}

val test1 : int -> nat effect {escape}

function test1(n) = {
  if (n < 0) then {
    throw (BadInput(n))
  };
  n
}

val test2 : int -> nat effect {escape}

function test2(n) = {
  m : nat = 0;
  if (n < 0) then {
    throw (BadInput(n))
  } else { m = 1 };
  n+m
}