fact: Definition check_exhaustiveness {A B} (ps_in : mlist (branch A B)) (ops : moption (mlist (branch A B))) : M (mlist (branch A B)) := '(mkInd_dyn _ _ _ constrs) <- M.constrs A; ( mfix2 f (ps : _) (constrs : _) : M _ := match ps, constrs with | mnil, mnil => match ops with | mNone => M.ret ps_in | mSome ps' => let ps := dreduce (@mapp) (mapp ps_in ps') in M.ret ps end | mcons p ps, _ => match p with | branch_app_static U C _ => constrs <- find_in_constrs C constrs; f ps constrs | _ => f ps constrs end | _, _ => M.raise (ConstrsUnmentioned constrs) end ) ps_in constrs .
imports: Mtac2(Base List Datatypes)