+ List.map
+ (fun (ind_uri,ind_obj) ->
+ add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
+ (!build_inversion_principle uri obj)
+
+let
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
+=
+ function
+ Cic.Fix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,idx,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n+1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.Fix (n,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ add_single_obj uri obj refinement_toolkit;
+ (n+1,uri::uris)
+ ) funs (1,[]))
+ | Cic.CoFix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n+1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.CoFix (n,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ add_single_obj uri obj refinement_toolkit;
+ (n+1,uri::uris)
+ ) funs (1,[]))
+ | _ -> assert false