fact: Definition classifier_to_dfa := {| dfa_s := imfun_of [::]; dfa_fin := [set x | cr (imfun_of_surj) x \in L]; dfa_trans x a := imfun_of (cr (imfun_of_surj) x ++ [::a]) |}.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa minimization regexp)