Module Termops

about contexts

Associates the contents of an identifier in a rel_context. Raise Not_found if there is no such identifier.

Functions that build argument lists matching a block of binders or a context. rel_vect n m builds |Rel (n+m);...;Rel(n+1)|

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_assum 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

Force the decomposition of a term as an applicative one

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

NOTE: to print terms you always want to use functions in Printer, not these ones which are for very special cases.