Language.SMTLib2.Internals.Type

data Type

type family Lifted (tps :: [Type]) (idx :: [Type]) :: [Type] where ...

class Unlift tps idx

type family Fst (a :: (p, q)) :: p where ...

type family Snd (a :: (p, q)) :: q where ...

class IsDatatype dt

type family CType (tp :: Type) (par :: [Type]) :: Type where ...

type family Instantiated (sig :: [Type]) (par :: [Type]) :: [Type] where ...

data ConApp dt par e

data AnyDatatype

data AnyConstr

data AnyField

data TypeRegistry dt con field

emptyTypeRegistry

dependencies

signature

constrSig

instantiate

ctype

determines

containedParameter

typeInference

typeInferences

partialInstantiation

partialInstantiations

registerType

registerTypeName

data DynamicDatatype par sig

data DynamicConstructor sig csig

data DynamicField sig tp

data DynamicValue plen sig par e

data BitWidth bw

getBw

data Value a

data AnyValue

data Repr t

data NumRepr t

data FunRepr sig

class GetType v

class GetFunType fun

bw

bool

int

real

bitvec

array

dt

dt'

showBitVec

valueType

liftType

numRepr

asNumRepr

getTypes

typeSize

typeFiniteDomain

withBW

bvAdd

bvSub

bvMul

bvDiv

bvMod

bvNegate

bvSignum

bvSucc

bvPred

bvMinValue

bvMaxValue

bwAdd

datatypeEq

datatypeCompare