Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | Safe-Infered |
This module implements normalization with respect to DH u AC using class
rewriting and an ad-hoc function that uses the TermAC
representation of
terms modulo AC.
- norm' :: LNTerm -> WithMaude LNTerm
- nf' :: LNTerm -> WithMaude Bool
- nfSubstVFresh' :: LNSubstVFresh -> WithMaude Bool
- normSubstVFresh' :: LNSubstVFresh -> WithMaude LNSubstVFresh
- maybeNotNfSubterms :: MaudeSig -> LNTerm -> [LNTerm]
Documentation
nfSubstVFresh' :: LNSubstVFresh -> WithMaude BoolSource
nfSubst s
returns True
if the substitution s
is in normal form.
normSubstVFresh' :: LNSubstVFresh -> WithMaude LNSubstVFreshSource
normSubst s
normalizes the substitution s
.
maybeNotNfSubterms :: MaudeSig -> LNTerm -> [LNTerm]Source
Returns all subterms that may be not in normal form.