diff options
| author | Gaëtan Gilbert | 2018-11-19 18:18:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-21 13:22:47 +0100 |
| commit | 9c678306157b2c6199091709ef7bb067f724f80c (patch) | |
| tree | 28bbb08c4500676b2eca478323243d867cf27c15 /kernel/indTyping.mli | |
| parent | 70ce3e98991a96f9d7f181a4a6f5b250457f1245 (diff) | |
Refactor typechecking of inductive types
We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
Diffstat (limited to 'kernel/indTyping.mli')
| -rw-r--r-- | kernel/indTyping.mli | 30 |
1 files changed, 19 insertions, 11 deletions
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index b16ada5ee8..8841e38636 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -8,17 +8,25 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names -open Constr open Environ +open Entries +open Declarations -val typecheck_inductive : - env -> - Entries.mutual_inductive_entry -> - env * env * rel_context * - (Id.t * Id.t list * types array * - (rel_context * - (bool * types * Univ.Universe.t, - Univ.Level.t option list * Univ.Universe.t) - Declarations.declaration_arity)) +(** Type checking for some inductive entry. + Returns: + - environment with inductives + parameters in rel context + - abstracted universes + - parameters + - for each inductive, + (arity * constructors) (with params) + * (indices * splayed constructor types) (both without params) + * allowed eliminations + *) +val typecheck_inductive : env -> mutual_inductive_entry -> + env + * abstract_inductive_universes + * Constr.rel_context + * ((inductive_arity * Constr.types array) * + (Constr.rel_context * (Constr.rel_context * Constr.types) array) * + Sorts.family list) array |