diff options
Diffstat (limited to 'lib/coq')
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 25a643e7..ee98c94e 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -27,6 +27,9 @@ Qed. Definition autocast {m n} (x : mword m) `{H:ArithFact (m = n)} : mword n := cast_mword x (use_ArithFact H). +Definition autocast_m {rv e m n} (x : monad rv (mword m) e) `{H:ArithFact (m = n)} : monad rv (mword n) e := + x >>= fun x => returnm (cast_mword x (use_ArithFact H)). + Definition cast_word {m n} (x : Word.word m) (eq : m = n) : Word.word n. rewrite <- eq. exact x. |