TPDB.DP.TCap

Documentation

tcap :: (Ord v, Ord c) => TRS v c -> Term v c -> Term Int c

This function keeps only those parts of the input term which cannot be reduced, even if the term is instantiated. All other parts are replaced by fresh variables. Def 4.4 in http://cl-informatik.uibk.ac.at/users/griff/publications/Sternagel-Thiemann-RTA10.pdf

fresh_var :: State Int (Term Int c)

walk :: (Ord a, Eq c) => RS s (Term a c) -> Term v c -> StateT Int Identity (Term Int c)