get_var i returns a var identified by its index i

fv t returns free variables of t

fv_l t returns free variables of t as a list

to_string t converts a term to its string representation

eta_conversion t applies η-conversion to t, if applicable

conversion a b t applies α-conversion to t replacing variable a with variable b

reduce_fix t applies β-reduction until there is no other reduction applicable

reduce_fix_timeout n t applies β-reduction until there is no other reduction * applicable or until n iterations reached

reduce n t applies n steps of β-reduction to t

has_redex t returns true if t has a β-reduction step

subst v t' t

len t returns the length of t