Language.Fixpoint.Types.Refinements

Representing Terms

data SymConst

data Constant

data Bop

data Brel

data Expr

type Pred

data KVar

data Subst

data Reft

data SortedReft

Constructing Terms

eVar

elit

eProp

pAnd

pOr

pIte

mkEApp

intKvar

vv_

Generalizing Embedding with Typeclasses

class Expression a

class Predicate a

class Subable a

class Reftable r

Constructors

reft

trueSortedReft

trueReft

falseReft

exprReft

notExprReft

uexprReft

symbolReft

usymbolReft

propReft

predReft

reftPred

reftBind

Predicates

isFunctionSortedReft

functionSort

isNonTrivial

isTautoPred

isSingletonReft

isEVar

isFalse

Destructing

flattenRefas

conjuncts

eApps

splitEApp

reftConjuncts

Transforming

mapPredReft

pprintReft