| Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
|---|---|
| Safe Haskell | Safe-Infered |
Term.Narrowing.Variants
Description
Computing and checking the variants of a term.
Documentation
computeVariantsCheck :: LNTerm -> WithMaude [LNSubstVFresh]Source
variantsListCheck ts computes all variants of ts considered as a single term
without a bound or symmetry substitution. Before returning the result, it checks
if the set of variants is complete and minimal. If that is not the case, it
fails with an error