summaryrefslogtreecommitdiff
path: root/test/ocaml
diff options
context:
space:
mode:
authorJon French2018-04-27 13:19:24 +0100
committerJon French2018-05-01 16:58:26 +0100
commitb94549367c2536b3df6fba8586efa1a2a4bca7b8 (patch)
tree73631c21df91613d96d1596e6d1add7d417abfe0 /test/ocaml
parentbf3a38a69fb895db274769b4d543976b07095d2f (diff)
further progress
Diffstat (limited to 'test/ocaml')
-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 f055a9b6..a9004297 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -4,6 +4,9 @@ type bits ('n : Int) = vector('n, dec, bit)
infix 4 ==
+val int : int <-> string
+overload int = string_of_int
+
val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool
val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
@@ -18,6 +21,7 @@ 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 eq_real = "eq_real" : (real, real) -> bool