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 /engine/termops.mli | |
| 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 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 6c680005d..5d812131e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -174,6 +174,16 @@ val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst val decompose_prod_letin : constr -> int * rel_context * constr val align_prod_letin : constr -> 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 + +(** Similar to [nb_prod], but zeta-contracts let-in on the way *) +val nb_prod_modulo_zeta : constr -> int + (** Get the last arg of a constr intended to be an application *) val last_arg : constr -> constr |