-let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
- let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
- let subst = [] in
- match obj with
- | Cic.InductiveDefinition (indTypes, params, leftno) ->
- let (name, inductive, ty, constructors) =
- try
- List.nth indTypes typeno
- with Failure _ -> assert false
- in
- let paramsno = count_pi ty in (* number of (left or right) parameters *)
- let rightno = paramsno - leftno in
- let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
- let conslen = List.length constructors in
- let consno = ref (conslen + 1) in
- if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then
- raise (Failure (sprintf "can't eliminate from Prop to %s"
- (string_of_sort sort)));
- let indty =
- let indty = Cic.MutInd (uri, typeno, subst) in
- if paramsno = 0 then
- indty
- else
- Cic.Appl (indty :: mk_rels 0 paramsno)
- in
- let mk_constructor consno =
- let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in
- if leftno = 0 then
- constructor
- else
- Cic.Appl (constructor :: mk_rels consno leftno)
- in
- let eliminator =
- let p_ty = type_of_p sort dependent leftno indty ty in
- let final_ty =
- add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty
- in
- Cic.Prod (Cic.Name "P", p_ty,
- (List.fold_right
- (fun (_, constructor) acc ->
- decr consno;
- let p = Cic.Rel !consno in
- Cic.Prod (Cic.Anonymous,
- (delta (uri, typeno, subst) dependent leftno !consno
- constructor p [mk_constructor !consno]),
- acc))
- constructors final_ty))
- in
- add_params leftno ty eliminator
- | _ -> assert false
-
-let rec branch (uri, typeno, subst) insource paramsno t fix head args =
- assert (subst = []);