fact: Definition log_input_handlers h inp st : list (disk_op log_files) * list output * log_state * list (name * msg) := let '(out, d, ps) := input_handlers h inp (log_data st) in log_handler_result (log_num_entries st) (inl inp) out d ps.
imports: Verdi(Verdi) Cheerios(Cheerios)