TPDB.Convert

Documentation

srs2trs :: SRS Identifier -> TRS Identifier Identifier

convert_srs_rule :: Rule [Identifier] -> Rule (Term Identifier Identifier)

trs2srs :: Eq v => TRS v s -> Maybe (SRS s)

convert_trs_rule :: Eq a => Rule (Term a s) -> Maybe (Rule [s])

unspine :: v -> [s] -> Term v s

spine :: Term v s -> Maybe ([s], v)

success iff term consists of unary symbols and the lowest node is a variable