diff options
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 |