Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
This module implements normalization and normal-form checks of terms.
- 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.