Module Termops

As occur_var but assume the identifier not to be a section variable

dependent m t tests whether m is a subterm of t

for visible vars only

Type assignment for metavariables

pop c lifts by -1 the positive indexes in c

replace_term_gen eq arity e c replaces matching subterms according to eq by e in c. If arity is non-zero applications of larger length are handled atomically.

subst_term d c replaces d by Rel 1 in c

replace_term d e c replaces d by e in c

Alternative term equalities

prod_applist forall (x1:B1;...;xn:Bn), B a1...an

returns

B[a1...an]

In prod_applist_decls n c args, c is supposed to have the form ∀Γ.c with Γ of length m and possibly with let-ins; it returns c with the assumptions of Γ instantiated by args and the local definitions of Γ expanded. Note that n counts both let-ins and prods, while the length of args only counts prods. In other words, varying n changes how many trailing let-ins are expanded.

Remove recursively the casts around a term i.e. strip_outer_cast (Cast (Cast ... (Cast c, t) ... )) is c.

nb_lam $ x_1:T_1...x_n:T_nc $ where $ c $ is not an abstraction gives $ n $ (casts are ignored)

Similar to nb_lam, but gives the number of products instead

Similar to nb_prod, but zeta-contracts let-in on the way

Get the last arg of a constr intended to be an application

name contexts

Set of local names

other signature iterators

Gives an ordered list of hypotheses, closed by dependencies, containing a given set

Test if an identifier is the basename of a global reference