Language.Fixpoint.Types.Refinements

Representing Terms

data SymConst

data Constant

data Bop

data Brel

data Expr

type Pred

data GradInfo

data KVar

data Subst

data KVSub

data Reft

data SortedReft

Constructing Terms

eVar

elit

eProp

pAnd

pOr

pIte

(&.&)

(|.|)

pExist

mkEApp

mkProp

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

isContraPred

isTautoPred

isSingletonReft

isFalse

Destructing

flattenRefas

conjuncts

eApps

eAppC

splitEApp

reftConjuncts

Transforming

mapPredReft

pprintReft

debruijnIndex

Gradual Type Manipulation

pGAnds

pGAnd

class HasGradual a

srcGradInfo