Term.Rewriting.Norm

This module implements normalization and normal-form checks of terms.

Documentation

norm' :: LNTerm -> WithMaude LNTerm

norm' t normalizes the term t using Maude.

nf' :: LNTerm -> WithMaude Bool

nf' t returns True if the term t is in normal form.

nfSubstVFresh' :: LNSubstVFresh -> WithMaude Bool

nfSubst s returns True if the substitution s is in normal form.

normSubstVFresh' :: LNSubstVFresh -> WithMaude LNSubstVFresh

normSubst s normalizes the substitution s.

maybeNotNfSubterms :: MaudeSig -> LNTerm -> [LNTerm]

Returns all subterms that may be not in normal form.