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