diff options
Diffstat (limited to 'model/prelude.sail')
| -rw-r--r-- | model/prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/model/prelude.sail b/model/prelude.sail index c09171a..22d050f 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -13,7 +13,7 @@ val string_take = "string_take" : (string, nat) -> string val string_length = "string_length" : string -> nat val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string -val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool +val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool overload operator == = {eq_string, eq_anything} @@ -57,7 +57,7 @@ function cast_unit_vec b = match b { bitone => 0b1 } -val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string +val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string val BitStr = "string_of_bits" : forall 'n. bits('n) -> string |