fact: Fixpoint has_eps e := match e with | Void => false | Eps => true | Dot => false | Atom x => false | Star e1 => true | Plus e1 e2 => has_eps e1 || has_eps e2 | And e1 e2 => has_eps e1 && has_eps e2 | Conc e1 e2 => has_eps e1 && has_eps e2 | Not e1 => ~~ (has_eps e1) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)