fact: Fixpoint deriv a i (e: ugregex'): ugregex' := match e with | u_prd _ => 0 | u_var j => ofbool (eqb_pos i j) | u_pls e f => deriv a i e + deriv a i f | u_dot e f => deriv a i e ⋅ f + ofbool (epsilon (set.mem a) e) ⋅ deriv a i f | u_itr e => deriv a i e ⋅ (e: ugregex')^* end.
imports: kat lsyntax positives sups glang comparisons boolean