Merge branch 'sail2' into mappings

1 files changed, 0 insertions, 30 deletions

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 78aab65e..0c5da675 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -194,36 +194,6 @@ let neq_bv l r = not (eq_bv l r)
 
 let inline neq_mword l r = (l <> r)
 
-val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r))
-let ulteq_bv l r = (eq_bv l r) || (ult_bv l r)
-let ugt_bv l r = not (ulteq_bv l r)
-let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r)
-
-val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let slt_bv l r =
-  match (most_significant l, most_significant r) with
-    | (B0, B0) -> ult_bv l r
-    | (B0, B1) -> false
-    | (B1, B0) -> true
-    | (B1, B1) ->
-       let l' = add_one_bit_ignore_overflow (bits_of l) in
-       let r' = add_one_bit_ignore_overflow (bits_of r) in
-       ugt_bv l' r'
-    | (BU, BU) -> ult_bv l r
-    | (BU, _) -> true
-    | (_, BU) -> false
-  end
-let slteq_bv l r = (eq_bv l r) || (slt_bv l r)
-let sgt_bv l r = not (slteq_bv l r)
-let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r)
-
-val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
-let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r)
-
-val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
-let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
-
 val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
 let get_slice_int_bv len n lo =
   let hi = lo + len - 1 in