summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-02-06 19:49:45 +0000
committerAlasdair Armstrong2019-02-06 19:49:45 +0000
commitcd6466eef8a7cb878010f5d9c6f6349606393bb1 (patch)
treee9e848a564d91101320f432acea09046366d874e
parentaadbe7ede88dc9bbbda6a09876baacd6797153fb (diff)
Add typechecking test from Mark
-rw-r--r--test/typecheck/pass/lt_flow.sail5
1 files changed, 5 insertions, 0 deletions
diff --git a/test/typecheck/pass/lt_flow.sail b/test/typecheck/pass/lt_flow.sail
new file mode 100644
index 00000000..4e7572da
--- /dev/null
+++ b/test/typecheck/pass/lt_flow.sail
@@ -0,0 +1,5 @@
+val lt_flow : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+val test : unit -> bool(true)
+
+function test() = lt_flow(1,10)