diff options
Diffstat (limited to 'lib/coq/Sail2_prompt_monad.v')
| -rw-r--r-- | lib/coq/Sail2_prompt_monad.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/coq/Sail2_prompt_monad.v b/lib/coq/Sail2_prompt_monad.v index b26a2ff3..0ff65d28 100644 --- a/lib/coq/Sail2_prompt_monad.v +++ b/lib/coq/Sail2_prompt_monad.v @@ -189,7 +189,7 @@ Definition read_memt_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memo Read_memt rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm. (*val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e*) -Definition read_memt {rv A B E} `{ArithFact (B >= 0)} rk (addr : mword A) sz : monad rv (mword B * bitU) E := +Definition read_memt {rv A B E} `{ArithFact (B >=? 0)} rk (addr : mword A) sz : monad rv (mword B * bitU) E := bind (read_memt_bytes rk addr sz) (fun '(bytes, tag) => @@ -203,7 +203,7 @@ Definition read_mem_bytes {rv A E} rk (addr : mword A) sz : monad rv (list memor Read_mem rk (Word.wordToNat (get_word addr)) (Z.to_nat sz) returnm. (*val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e*) -Definition read_mem {rv A B E} `{ArithFact (B >= 0)} rk (addrsz : Z) (addr : mword A) sz : monad rv (mword B) E := +Definition read_mem {rv A B E} `{ArithFact (B >=? 0)} rk (addrsz : Z) (addr : mword A) sz : monad rv (mword B) E := bind (read_mem_bytes rk addr sz) (fun bytes => |