diff options
| author | Jon French | 2018-09-14 15:08:30 +0100 |
|---|---|---|
| committer | Jon French | 2018-09-14 15:08:55 +0100 |
| commit | 959473a1b881729eacd993dbeee193396b031bd5 (patch) | |
| tree | f6cd18f10cddb98156b6a720e00c4b7946f94591 /riscv | |
| parent | bd7c2be6fe9cb955e25e04d59c5af089a04bcf9e (diff) | |
RISCV prelude: fix typo in ocaml extern for negate_*
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index a073b20f..9ecc35a0 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -300,9 +300,9 @@ val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real -val negate_range = {ocaml: "minus_big_int", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) +val negate_range = {ocaml: "negate", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) -val negate_int = {ocaml: "minus_big_int", lem: "integerNegate", coq: "Z.opp"} : int -> int +val negate_int = {ocaml: "negate", lem: "integerNegate", coq: "Z.opp"} : int -> int val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real |