| 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.
- checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc
- checkSortedReftFull :: SEnv SortedReft -> SortedReft -> Maybe Doc
- pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft
Checking Well-Formedness
checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe DocSource
Checking Refinements -----------------------------------------------
pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReftSource