diff options
Diffstat (limited to 'prover_snapshots/hol4/lib/sail/sail2_state_monadScript.sml')
| -rw-r--r-- | prover_snapshots/hol4/lib/sail/sail2_state_monadScript.sml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/prover_snapshots/hol4/lib/sail/sail2_state_monadScript.sml b/prover_snapshots/hol4/lib/sail/sail2_state_monadScript.sml index 6af7a24..a504cca 100644 --- a/prover_snapshots/hol4/lib/sail/sail2_state_monadScript.sml +++ b/prover_snapshots/hol4/lib/sail/sail2_state_monadScript.sml @@ -226,10 +226,9 @@ val _ = Define ` (let addrs = (GENLIST (\ n . addr + n) sz) in let a_v = (lem_list$list_combine addrs v) in let write_byte = (\mem p . (case (mem ,p ) of - ( mem , (addr, v) ) => mem |+ ( addr , - v ) + ( mem , (addr, v) ) =>mem |+ (addr, v) )) in - let write_tag = (\ mem addr . mem |+ ( addr , tag )) in + let write_tag = (\ mem addr . mem |+ (addr, tag)) in ( s with<| memstate := (FOLDL write_byte s.memstate a_v); tagstate := (FOLDL write_tag s.tagstate addrs) |>)))`; |