diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a08136424..d0dee30b9 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -64,6 +64,9 @@ type mutual_inductive_entry = { mind_entry_finite : bool; mind_entry_inds : (identifier * constr * identifier list * constr) list } +(*s The different kinds of errors that may result of a malformed inductive + definition. *) + type inductive_error = | NonPos of int | NotEnoughArgs of int @@ -76,6 +79,9 @@ type inductive_error = exception InductiveError of inductive_error +(*s The following functions are utility functions to check and to + decompose a declaration. *) + (* [mind_check_names] checks the names of an inductive types declaration i.e. that all the types and constructors names are distinct. It raises an exception [InductiveError _] if it is not the case. *) @@ -92,5 +98,4 @@ val mind_extract_and_check_params : val mind_extract_params : int -> constr -> (name * constr) list * constr - val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit |