(* creates the discrimination = injection+contradiction principle *)
exception ConstructorTooBig of string;;
-let mk_discriminator ~use_jmeq name it leftno status baseuri =
+let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri =
let itnargs =
let _,_,arity,_ = it in
List.length (arg_list 0 arity) in
List.map
(fun i ->
let nargs_kty = nargs it leftno i in
- if (nargs_kty > 5 && not use_jmeq) then raise (ConstructorTooBig (kname i));
+ if (nargs_kty > 5 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i));
let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc)
(nargs_kty - 1) [] in
let nones =
(* PHASE 2: create the object for the proof of the principle: we'll name it
* "theorem" *)
let status, theorem =
- GrafiteDisambiguate.disambiguate_nobj status ~baseuri
+ let attrs = `Generated, `Theorem, `DiscriminationPrinciple in
+ GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",0,
NotationPt.Theorem
- (`Theorem,name,principle,
- Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple))
+ (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
in
let uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in