Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|

Safe Haskell | None |

Computing the variants of a term.

- computeVariantsBound :: LNTerm -> Maybe Int -> WithMaude (Maybe [LNSubstVFresh])
- computeVariants :: LNTerm -> WithMaude [LNSubstVFresh]
- compareSubstVariant :: LNTerm -> LNSubstVFresh -> LNSubstVFresh -> WithMaude (Maybe Ordering)

# Documentation

computeVariantsBound :: LNTerm -> Maybe Int -> WithMaude (Maybe [LNSubstVFresh])Source

`computeVariants t d`

compute the variants of term `t`

with bound `d`

.
The rewriting rules are taken from the Maude context.

computeVariants :: LNTerm -> WithMaude [LNSubstVFresh]Source

`variantsList ts`

computes all variants of `ts`

considered as a single term
without a bound or symmetry substitution.
The rewriting rules are taken from the Maude context.

# for testing

compareSubstVariant :: LNTerm -> LNSubstVFresh -> LNSubstVFresh -> WithMaude (Maybe Ordering)Source

`substCompareVariant t s1 t2`

compares two substitutions using the variant order
with respect to `t`

.