Language.Fixpoint.Types.Constraints

Top-level Queries

type FInfo a

type SInfo a

data GInfo c a

data FInfoWithOpts a

convertFormat

type Solver a

Serializing

toFixpoint

writeFInfo

saveQuery

Constructing Queries

fi

Constraints

data WfC a

isGWfc

updateWfCExpr

data SubC a

type SubcId

mkSubC

subcId

sid

senv

slhs

srhs

stag

subC

wfC

data SimpC a

type Tag

class TaggedC c a

clhs

crhs

strengthenLhs

Accessing Constraints

addIds

sinfo

shiftVV

Qualifiers

data Qualifier

trueQual

qualifier

mkQual

remakeQual

Results

type FixSolution

type GFixSolution

toGFixSol

data Result a

Cut KVars

data Kuts

ksMember

Higher Order Logic

data HOInfo

allowHO

allowHOquals

Axioms

data AxiomEnv

data Equation

data Rewrite

getEqBody