type id = string;;
type joint_recursion_kind =
- [ `Recursive
+ [ `Recursive of int list
| `CoRecursive
| `Inductive of int (* paramsno *)
| `CoInductive of int (* paramsno *)
}
and 'term arg =
- Aux of int
+ Aux of string
| Premise of premise
+ | Lemma of lemma
| Term of 'term
| ArgProof of 'term proof
| ArgMethod of string (* ???? *)
premise_binder : string option;
premise_n : int option;
}
+
+and lemma =
+ { lemma_id: string;
+ lemma_name: string;
+ lemma_uri: string
+ }
+
;;
type 'term conjecture = id * int * 'term context * 'term