diff options
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index edd4eb231..ada268606 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -30,16 +30,22 @@ type case_printing = cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *) style : case_style } -(** the integer is the number of real args, needed for reduction *) +(* INVARIANT: + * - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs + * - forall (i : 0 .. pred (Array.length ci_cstr_ndecls)), + * ci_cstr_ndecls.(i) >= ci_cstr_nargs.(i) + *) type case_info = { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *) ci_npar : int; (* number of parameters of the above inductive type *) - ci_cstr_ndecls : int array; (* number of arguments of individual constructors - (numbers of parameters of the inductive type are excluded from the count) - (with let's) *) - ci_cstr_nargs : int array; (* number of arguments of individual constructors - (numbers of parameters of the inductive type are excluded from the count) - (w/o let's) *) + ci_cstr_ndecls : int array; (* For each constructor, the corresponding integer determines + the number of values that can be bound in a match-construct. + NOTE: parameters of the inductive type are therefore excluded from the count *) + ci_cstr_nargs : int array; (* for each constructor, the corresponding integers determines + the number of values that can be applied to the constructor, + in addition to the parameters of the related inductive type + NOTE: "lets" are therefore excluded from the count + NOTE: parameters of the inductive type are also excluded from the count *) ci_pp_info : case_printing (* not interpreted by the kernel *) } |