Coq: support if-then-throw typechecking special case

1 files changed, 25 insertions, 0 deletions

diff --git a/test/coq/pass/throw_fact.sail b/test/coq/pass/throw_fact.sail
new file mode 100644
index 00000000..e40267b1
--- /dev/null
+++ b/test/coq/pass/throw_fact.sail
@@ -0,0 +1,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
+}