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_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.

Lightweight first-order filtering procedure. Unification variables ar represented by (untyped) Evars. filtering c1 c2 returns the substitution n'th evar -> (context,term), or raises CannotFilter. Warning: Outer-kernel sort subtyping are taken into account: c1 has to be smaller than c2 wrt. sorts.

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