fact: Definition scan (events : seq event) (bottom top : edge) : seq cell := match events with | [::] => [:: complete_last_open bottom top (start_open_cell bottom top)] | ev0 :: events => let start_scan := start ev0 bottom top in let final_scan := iter_list step events start_scan in map (complete_last_open bottom top) (lst_open final_scan :: sc_open1 final_scan ++ sc_open2 final_scan) ++ lst_closed final_scan :: sc_closed final_scan end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL