Copilot.Compile.SBV.Witness

Documentation

data SymWordInst a

Constructors

SymWord a => SymWordInst

symWordInst :: Type a -> SymWordInst a

data NumInst a

Constructors

Num a => NumInst

numInst :: Type a -> NumInst a

data HasSignAndSizeInst a

Constructors

SymWord a => HasSignAndSizeInst

hasSignAndSizeInst :: Type a -> HasSignAndSizeInst a

data EqInst a

Constructors

EqSymbolic (SBV a) => EqInst

eqInst :: Type a -> EqInst a

data CastInst a b

Constructors

SBVCast a b => CastInst

castInst :: Type a -> Type b -> CastInst a b

sbvCast :: SBVCast a b => SBV a -> SBV b

data BVDivisibleInst a

Constructors

SDivisible (SBV a) => BVDivisibleInst

divInst :: Type a -> BVDivisibleInst a

data OrdInst a

Constructors

OrdSymbolic (SBV a) => OrdInst

ordInst :: Type a -> OrdInst a

data MergeableInst a

Constructors

Mergeable (SBV a) => MergeableInst

mergeableInst :: Type a -> MergeableInst a

data BitsInst a

Constructors

(Bits a, Bits (SBV a)) => BitsInst

bitsInst :: Type a -> BitsInst a

data IntegralInst a

Constructors

SIntegral a => IntegralInst

integralInst :: Type a -> IntegralInst a