Language.Fixpoint.Types.Refinements
data SymConst
data Constant
data Bop
data Brel
data Expr
type Pred
data KVar
data Subst
data Reft
data SortedReft
eVar
elit
eProp
pAnd
pOr
pIte
mkEApp
intKvar
vv_
class Expression a
class Predicate a
class Subable a
class Reftable r
reft
trueSortedReft
trueReft
falseReft
exprReft
notExprReft
uexprReft
symbolReft
usymbolReft
propReft
predReft
reftPred
reftBind
isFunctionSortedReft
functionSort
isNonTrivial
isTautoPred
isSingletonReft
isEVar
isFalse
flattenRefas
conjuncts
eApps
splitEApp
reftConjuncts
mapPredReft
pprintReft