summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorJon French2018-04-30 15:18:56 +0100
committerJon French2018-05-01 16:58:26 +0100
commitf8abc90f5e7ae8e25f2750a186eee2ef30021cf5 (patch)
tree907ab7b81234f4bcf5cdede79c6a96e0cccb3edd /test
parent274204a6f36d7c62a2030ed72f47d07f60c23a34 (diff)
further progress but confounds the type checker?
Diffstat (limited to 'test')
-rw-r--r--test/ocaml/prelude.sail4
1 files changed, 4 insertions, 0 deletions
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
index a9004297..54c88cb8 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -17,11 +17,15 @@ val eq_int = "eq_int" : (int, int) -> bool
val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool
+union option ('a : Type) = {None : unit, Some : 'a}
+
val eq_string = "eq_string" : (string, string) -> bool
val string_startswith = "string_startswith" : (string, string) -> bool
val string_drop = "string_drop" : (string, nat) -> string
val string_length = "string_length" : string -> nat
val string_append = "string_append" : (string, string) -> string
+val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat))
+val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat))
val eq_real = "eq_real" : (real, real) -> bool