Language.Fixpoint.Sort

This module has the functions that perform sort-checking, and related operations on Fixpoint expressions and predicates.

Checking Well-Formedness

checkSorted :: Checkable a => SEnv Sort -> a -> Maybe Doc

checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc

Checking Refinements -----------------------------------------------

checkSortedReftFull :: Checkable a => SEnv SortedReft -> a -> Maybe Doc

checkSortFull :: Checkable a => SEnv SortedReft -> Sort -> a -> Maybe Doc

pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft