diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-08 09:54:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 08:58:20 +0100 |
| commit | 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 (patch) | |
| tree | fc399b19682aa528a73d90729c1e37ce4a761d6e /kernel | |
| parent | f22ad605a14eb14d11b0a1615f7014f2dca3b483 (diff) | |
Moving three related small half-general half-ad-hoc utility functions
next to each other, waiting for possible integration into a more
uniform API.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 19 | ||||
| -rw-r--r-- | kernel/term.mli | 7 |
2 files changed, 0 insertions, 26 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 33ed25fe1..7d47c4609 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -616,25 +616,6 @@ let decompose_lam_n_decls n = in lamdec_rec empty_rel_context n -(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction - * gives n (casts are ignored) *) -let nb_lam = - let rec nbrec n c = match kind_of_term c with - | Lambda (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - -(* similar to nb_lam, but gives the number of products instead *) -let nb_prod = - let rec nbrec n c = match kind_of_term c with - | Prod (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - let prod_assum t = fst (decompose_prod_assum t) let prod_n_assum n t = fst (decompose_prod_n_assum n t) let strip_prod_assum t = snd (decompose_prod_assum t) diff --git a/kernel/term.mli b/kernel/term.mli index 2bb811060..69adb517a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -308,13 +308,6 @@ val decompose_lam_n_assum : int -> constr -> rel_context * constr (** Idem, counting let-ins *) val decompose_lam_n_decls : int -> constr -> rel_context * constr -(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction - gives {% $ %}n{% $ %} (casts are ignored) *) -val nb_lam : constr -> int - -(** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : constr -> int - (** Return the premisses/parameters of a type/term (let-in included) *) val prod_assum : types -> rel_context val lam_assum : constr -> rel_context |