fact: Fixpoint words_go (cur : option string) (s : string) : list string := match s with | "" => option_list (string_rev <$> cur) | String a s => if is_space a then option_list (string_rev <$> cur) ++ words_go None s else words_go (Some (from_option (String a) (String a "") cur)) s end.
imports: Coq(Ascii) stdpp(countable) stdpp(options)