add_n_lambdas n t returns the term t with n (extra) anonymous lambda abstraction. Doesn't shift free variables of t.

term_eq t t' is true if t = t' (up to alpha equivalence)

Position in a term

subterm t p returns the subterm of t at position p. Raises InvalidSubterm in case of invalid position in given term.

Type for comparison functions

compare_term id_comp t t' compares both terms (up to alpha equivalence). * The order relation goes : * Kind < Type < Const < DB < App < Lam < Pi * Besides * Const m v < Const m' v' iif (m,v) < (m',v') * DB n < DB n' iif n < n' * App f a args < App f' a' args' iif (f,a,args) < (f',a',args') * Lam x ty t < Lam x' ty' t' iif t < t' * Pi x a b < Pi x' a' b' iif (a,b) < (a',b')

Return true iff given algebra is AC or ACU.

Constraints (n,t,u) are t=u under n lambdas

General context: variables have abstract annotations

Partially annotated context: as generated at rule parsing

Fully type annotated context: as generated by type checking

Arity annotated context: used for rewriting in untyped setting

(n, t) represents the term represented by t * (whichever its representation) under n lambda abstractions.