diff options
| author | Robert Norton <rmn30@cam.ac.uk> | 2019-07-01 12:09:02 +0100 |
|---|---|---|
| committer | Robert Norton <rmn30@cam.ac.uk> | 2019-07-01 12:09:02 +0100 |
| commit | b3a9c7972d7c75b0e133f11def12c3c9f1a090f9 (patch) | |
| tree | a6fe631a62c8cb19b364fd8779c8ff6154e280c1 /model/prelude.sail | |
| parent | efdbcdb53c9f11cf259443c5768fff168cfe50a0 (diff) | |
| parent | 0fbfc08351dfdc2f57c57f78632ce9bef64d109a (diff) | |
| download | sail-riscv-b3a9c7972d7c75b0e133f11def12c3c9f1a090f9.zip sail-riscv-b3a9c7972d7c75b0e133f11def12c3c9f1a090f9.tar.gz sail-riscv-b3a9c7972d7c75b0e133f11def12c3c9f1a090f9.tar.bz2 | |
Merge remote-tracking branch 'origin/master' into master-cleanup
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 |