fact: Fixpoint re_lang (char: eqType) (e : regexp char) : dlang char := match e with | Void => void char | Eps => eps char | Atom x => atom x | Star e1 => star (re_lang e1) | Plus e1 e2 => plus (re_lang e1) (re_lang e2) | Conc e1 e2 => conc (re_lang e1) (re_lang e2) end.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)