diff options
| author | Robert Norton <rmn30@cam.ac.uk> | 2019-06-20 13:21:04 +0100 |
|---|---|---|
| committer | Robert Norton <rmn30@cam.ac.uk> | 2019-06-20 13:21:04 +0100 |
| commit | c4260c12c978866d8701156695140cfaf7c6dc68 (patch) | |
| tree | 097c3078328b3ed8c08545ce3d550b83d9777d03 /model/prelude.sail | |
| parent | 36f5da6a169afaba86d2c7191df477ae1837d5d1 (diff) | |
| download | sail-riscv-c4260c12c978866d8701156695140cfaf7c6dc68.zip sail-riscv-c4260c12c978866d8701156695140cfaf7c6dc68.tar.gz sail-riscv-c4260c12c978866d8701156695140cfaf7c6dc68.tar.bz2 | |
Add interpreter builtin for min_nat. Should min/max be in standard library?
Diffstat (limited to 'model/prelude.sail')
| -rw-r--r-- | model/prelude.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/model/prelude.sail b/model/prelude.sail index 51ed984..54f7d03 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -79,7 +79,7 @@ val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", le /* The following should get us euclidean modulus, and is compatible with pre and post 0.9 versions of sail */ overload operator % = {emod_int, mod} -val min_nat = {ocaml: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat +val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int |