Return the list of all function symbols in the term, from left to right.

>>> funs (Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]])
"fgf"

Difference List version of funs. We have funsDL t vs = funs t ++ vs.

Return the list of all variables in the term, from left to right.

>>> vars (Fun 'g' [Var 3, Fun 'f' [Var 1, Var 2, Var 3]])
[3,1,2,3]

Difference List version of vars. We have varsDL t vs = vars t ++ vs.

Return the root symbol of the given term.

>>> root (Fun 'f' [Var 1, Fun 'g' []])
Right 'f'

>>> root (Var 1)
Left 1

Annotate each occurrence of a function symbol with its actual arity, i.e., its number of arguments.

>>> withArity (Fun 'f' [Var 1, Fun 'f' []])
Fun ('f',2) [Var 1,Fun ('f',0) []]

Return the subterm at a given position.

Return the list of all proper subterms.

>>> properSubterms (Fun 'g' [Fun 'f' [Var 1], Fun 'f' [Var 1]])
[Fun 'f' [Var 1],Var 1,Fun 'f' [Var 1],Var 1]

Return the list of all subterms.

subterms t = t : properSubterms t

replace a subterm at a given position.

Rename the variables in a term.

>>> rename (+ 1) (Fun 'f' [Var 1, Fun 'g' [Var 2]])
(Fun 'f' [Var 2, Fun 'g' [Var 3]])

Return True if the term is a variable, False otherwise.

Return True if the term is a function application, False otherwise.

Check whether the term is a ground term, i.e., contains no variables.

Check whether the term is linear, i.e., contains each variable at most once.

Check whether the first term is an instance of the second term.

Check whether two terms are variants of each other.