diff options
Diffstat (limited to 'handwritten_support/mem_metadata.v')
| -rw-r--r-- | handwritten_support/mem_metadata.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v index 0e53888..e70d395 100644 --- a/handwritten_support/mem_metadata.v +++ b/handwritten_support/mem_metadata.v @@ -6,6 +6,6 @@ Require Import Sail2_prompt. Definition write_ram {rv e a} wk (addr : mword a) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk a addr size v. -Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e := +Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size) * unit) e := read_mem rk a addr size >>= fun data => returnm (data, tt). |