fact: Definition construct_case A (x: A) (loop: forall r: dynr, M (moption (result x (elemr r)))) C := let 'mkCase _ val retrn branches := C in nu (FreshFromStr "v") mNone (fun v=> new_val_opt <- loop (Dynr val); '(m: some_branch_depends, new_branches) <- M.fold_right ( fun branch '(m: some_branch_depends, new_branches) => b <- to_dynr branch; r <- loop b; match r with | mSome r => let (fub, _) := r in let fub := reduce (RedWhd [rl:RedBeta]) (fub v) in ret (m: true, Dyn fub :m: new_branches) | mNone => ret (m: some_branch_depends, branch :m: new_branches) end ) (m: false, [m:]) branches; let new_val := match new_val_opt with mSome new_val => new_val | mNone => R (fun _ => val) meq_refl end in match new_val_opt, some_branch_depends with | mSome _, _ | _, true => let (fuv, _) := new_val in let fuv := reduce (RedWhd [rl:RedBeta]) (fuv v) in let new_case := reduce_dyns {| case_val := fuv; case_return := retrn; case_branches := new_branches |} in d <- makecase new_case; dcase d as A0, cas in func <- abs_fun v cas; ret (mSome (@Dyn (A -> A0) func)) | _,_ => ret mNone end ).
imports: Mtac2(Base Logic Datatypes List) Strings.String