fact: Definition disk_to_channel (dsk : do_disk file_name) := fun file => (match dsk file with | Some s => Some (IOStreamWriter.channel_send (IOStreamWriter.out_channel_wrap s)) | None => None end).
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)