diff options
Diffstat (limited to 'src/gen_lib/sail_values.lem')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index ace65b3b..fa2afe23 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -434,18 +434,25 @@ let eq (l,r) = bool_to_bit (l = r) let eq_vec_range (l,r) = eq (to_num false l,r) let eq_range_vec (l,r) = eq (l, to_num false r) let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) - -let neq (l,r) = bitwise_not_bit (eq (l,r)) +(* +let neq (l,r) = bitwise_not_bit (eq (l,r)) *) let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r)) let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r)) let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r)) +(* temporarily *) +val neq : forall 'a 'b. 'a * 'b -> bit +let neq _ = O + + let EXTS (v1,(V _ _ is_inc as v)) = to_vec is_inc (v1,signed v) let EXTZ = EXTS +let exts = EXTS + val make_indexed_vector_reg : list (integer * register) -> maybe register -> integer -> integer -> vector register let make_indexed_vector_reg entries default start length = |