diff options
Diffstat (limited to 'aarch64')
| -rwxr-xr-x | aarch64/prelude.sail | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 505ca7b6..98318dd4 100755 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -127,7 +127,7 @@ val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec"} : forall 'n. (bits function and_vec (xs, ys) = builtin_and_vec(xs, ys) -overload operator & = {and_bool, and_vec} +overload operator & = {and_vec} val builtin_or_vec = {ocaml: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n) @@ -264,19 +264,19 @@ val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt", c: "sqrt_real", coq: "sqrt"} : val gteq_real = {ocaml: "gteq_real", lem: "gteq", c: "gteq_real", coq: "gteq_real"} : (real, real) -> bool -overload operator >= = {gteq_atom, gteq_int, gteq_real} +overload operator >= = {gteq_real} val lteq_real = {ocaml: "lteq_real", lem: "lteq", c: "lteq_real", coq: "lteq_real"} : (real, real) -> bool -overload operator <= = {lteq_atom, lteq_int, lteq_real} +overload operator <= = {lteq_real} val gt_real = {ocaml: "gt_real", lem: "gt", c: "gt_real", coq: "gt_real"} : (real, real) -> bool -overload operator > = {gt_atom, gt_int, gt_real} +overload operator > = {gt_real} val lt_real = {ocaml: "lt_real", lem: "lt", c: "lt_real", coq: "lt_real"} : (real, real) -> bool -overload operator < = {lt_atom, lt_int, lt_real} +overload operator < = {lt_real} val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down", coq: "Zfloor"} : real -> int |