diff options
| author | Hugo Herbelin | 2020-04-13 00:47:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-09 11:04:47 +0100 |
| commit | 3f286f3fcb846cac360969372d71e91c5aefe810 (patch) | |
| tree | ab4ff9b39ab12c43332bb290c8f6e971f6391a70 | |
| parent | a386c2f1ba38ea106a1da386eddd029bd9b66e37 (diff) | |
Adding functions to returning the def/decl status of an inductive arity.
| -rw-r--r-- | pretyping/inductiveops.ml | 8 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 4 |
2 files changed, 12 insertions, 0 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 23145b1629..bd875cf68b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) = let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u) [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] +let inductive_alltags env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Context.Rel.to_tags mip.mind_arity_ctxt + +let constructor_alltags env (ind,j) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1)) + let constructor_has_local_defs env (indsp,j) = let (mib,mip) = Inductive.lookup_mind_specif env indsp in let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1e2bba9f73..3705d39280 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -138,6 +138,10 @@ val constructor_nrealdecls : env -> constructor -> int val constructor_nrealdecls_env : env -> constructor -> int [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] +(** @return tags of all decls: true = assumption, false = letin *) +val inductive_alltags : env -> inductive -> bool list +val constructor_alltags : env -> constructor -> bool list + (** Is there local defs in params or args ? *) val constructor_has_local_defs : env -> constructor -> bool val inductive_has_local_defs : env -> inductive -> bool |