Safe Haskell	None
Language	Haskell2010

What4.IndexLit

Synopsis

data IndexLit idx where
- IntIndexLit :: !Integer -> IndexLit BaseIntegerType
- BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w)
hashIndexLit :: Int -> IndexLit idx -> Int

Documentation

data IndexLit idx where Source #

This represents a concrete index value, and is used for creating arrays.

Constructors

IntIndexLit :: !Integer -> IndexLit BaseIntegerType
BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w)

Instances

Instances details

TestEquality IndexLit Source #
Instance details Defined in What4.IndexLit Methods testEquality :: forall (a :: k) (b :: k). IndexLit a -> IndexLit b -> Maybe (a :~: b) #
OrdF IndexLit Source #
Instance details Defined in What4.IndexLit Methods compareF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool # ltF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool # geqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool # gtF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool #
ShowF IndexLit Source #
Instance details Defined in What4.IndexLit Methods withShow :: forall p q (tp :: k) a. p IndexLit -> q tp -> (Show (IndexLit tp) => a) -> a # showF :: forall (tp :: k). IndexLit tp -> String # showsPrecF :: forall (tp :: k). Int -> IndexLit tp -> String -> String #
HashableF IndexLit Source #
Instance details Defined in What4.IndexLit Methods hashWithSaltF :: forall (tp :: k). Int -> IndexLit tp -> Int # hashF :: forall (tp :: k). IndexLit tp -> Int #
Eq (IndexLit tp) Source #
Instance details Defined in What4.IndexLit Methods (==) :: IndexLit tp -> IndexLit tp -> Bool # (/=) :: IndexLit tp -> IndexLit tp -> Bool #
Show (IndexLit tp) Source #
Instance details Defined in What4.IndexLit Methods showsPrec :: Int -> IndexLit tp -> ShowS # show :: IndexLit tp -> String # showList :: [IndexLit tp] -> ShowS #
Hashable (IndexLit tp) Source #
Instance details Defined in What4.IndexLit Methods hashWithSalt :: Int -> IndexLit tp -> Int # hash :: IndexLit tp -> Int #

hashIndexLit :: Int -> IndexLit idx -> Int Source #