summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/coq/pass/booltyparam.sail11
1 files changed, 11 insertions, 0 deletions
diff --git a/test/coq/pass/booltyparam.sail b/test/coq/pass/booltyparam.sail
new file mode 100644
index 00000000..423c2720
--- /dev/null
+++ b/test/coq/pass/booltyparam.sail
@@ -0,0 +1,11 @@
+/* Test a boolean type parameter. Not sure that this is terribly useful,
+ but it fills a gap in coverage... */
+
+$include <prelude.sail>
+
+union perhaps('b : Bool) = {No : unit, Yes : {'n, 'b. atom('n)}}
+
+val foo : forall 'n. atom('n) -> perhaps('n >= 0)
+
+function foo(n) =
+ if n >= 0 then Yes(n) else No()