diff options
Diffstat (limited to 'lib/string.sail')
| -rw-r--r-- | lib/string.sail | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/lib/string.sail b/lib/string.sail index 3fe74eb5..9e6044b9 100644 --- a/lib/string.sail +++ b/lib/string.sail @@ -5,17 +5,17 @@ $include <arith.sail> val eq_string = {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string) -> bool -infixl 9 ^-^ +overload operator == = {eq_string} -val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string +val concat_str = {coq: "String.append", lem: "stringAppend", _: "concat_str"} : (string, string) -> string val "dec_str" : int -> string val "hex_str" : int -> string -val bits_str = "string_of_bits" : forall 'n. vector('n, dec, bit) -> string +val bits_str = "string_of_bits" : forall 'n. bitvector('n, dec) -> string -val concat_str_bits : forall 'n. (string, vector('n, dec, bit)) -> string +val concat_str_bits : forall 'n. (string, bitvector('n, dec)) -> string function concat_str_bits(str, x) = concat_str(str, bits_str(x)) @@ -23,8 +23,6 @@ val concat_str_dec : (string, int) -> string function concat_str_dec(str, x) = concat_str(str, dec_str(x)) -overload operator ^-^ = {concat_str, concat_str_bits, concat_str_dec} - val print_endline = "print_endline" : string -> unit val prerr_endline = "prerr_endline" : string -> unit |