| Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
|---|---|
| Safe Haskell | Safe-Infered |
Term.Narrowing.Variants.Compute
Contents
Description
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.