fact: Definition update_disk (dsk : do_disk file_name) (op : disk_op file_name) : do_disk file_name := match op with | Append file x => update file_name_eq_dec dsk file (match dsk file with | Some s => Some (s +$+ x) | None => Some x end) | Write file x => update file_name_eq_dec dsk file (Some x) | Delete file => update file_name_eq_dec dsk file (Some IOStreamWriter.empty) end.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)