Safe Haskell	None
Language	Haskell2010

What4.IndexLit

Synopsis

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

Documentation

data IndexLit (idx :: BaseType) where Source #

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

Constructors

IntIndexLit :: !Integer -> IndexLit 'BaseIntegerType
BVIndexLit :: forall (w :: Natural). 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 :: BaseType) (b :: BaseType). IndexLit a -> IndexLit b -> Maybe (a :~: b) #
HashableF IndexLit Source #
Instance details Defined in What4.IndexLit Methods hashWithSaltF :: forall (tp :: BaseType). Int -> IndexLit tp -> Int # hashF :: forall (tp :: BaseType). IndexLit tp -> Int #
OrdF IndexLit Source #
Instance details Defined in What4.IndexLit Methods compareF :: forall (x :: BaseType) (y :: BaseType). IndexLit x -> IndexLit y -> OrderingF x y # leqF :: forall (x :: BaseType) (y :: BaseType). IndexLit x -> IndexLit y -> Bool # ltF :: forall (x :: BaseType) (y :: BaseType). IndexLit x -> IndexLit y -> Bool # geqF :: forall (x :: BaseType) (y :: BaseType). IndexLit x -> IndexLit y -> Bool # gtF :: forall (x :: BaseType) (y :: BaseType). IndexLit x -> IndexLit y -> Bool #
ShowF IndexLit Source #
Instance details Defined in What4.IndexLit Methods withShow :: forall p q (tp :: BaseType) a. p IndexLit -> q tp -> (Show (IndexLit tp) => a) -> a # showF :: forall (tp :: BaseType). IndexLit tp -> String # showsPrecF :: forall (tp :: BaseType). Int -> IndexLit tp -> String -> String #
Show (IndexLit tp) Source #
Instance details Defined in What4.IndexLit Methods showsPrec :: Int -> IndexLit tp -> ShowS # show :: IndexLit tp -> String # showList :: [IndexLit tp] -> ShowS #
Eq (IndexLit tp) Source #
Instance details Defined in What4.IndexLit Methods (==) :: IndexLit tp -> IndexLit tp -> Bool # (/=) :: IndexLit tp -> IndexLit tp -> Bool #
Hashable (IndexLit tp) Source #
Instance details Defined in What4.IndexLit Methods hashWithSalt :: Int -> IndexLit tp -> Int # hash :: IndexLit tp -> Int #

hashIndexLit :: forall (idx :: BaseType). Int -> IndexLit idx -> Int Source #