| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Sort
Description
This module has the functions that perform sort-checking, and related operations on Fixpoint expressions and predicates.
- data TVSubst
- checkSorted :: Checkable a => SEnv Sort -> a -> Maybe Doc
- checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc
- checkSortedReftFull :: Checkable a => SEnv SortedReft -> a -> Maybe Doc
- checkSortFull :: Checkable a => SEnv SortedReft -> Sort -> a -> Maybe Doc
- pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft
- unify :: Sort -> Sort -> Maybe TVSubst
- apply :: TVSubst -> Sort -> Sort
Sort Substitutions
Checking Well-Formedness
checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc Source
Checking Refinements -----------------------------------------------
checkSortedReftFull :: Checkable a => SEnv SortedReft -> a -> Maybe Doc Source
checkSortFull :: Checkable a => SEnv SortedReft -> Sort -> a -> Maybe Doc Source
pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft Source