what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Safe Haskell | Safe-Inferred
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) Source #
HashableF IndexLit Source # |
Instance details Defined in What4.IndexLit Methods hashWithSaltF :: forall (tp :: k). Int -> IndexLit tp -> Int Source # hashF :: forall (tp :: k). IndexLit tp -> Int Source #
OrdF IndexLit Source # |

Instance details

Defined in What4.IndexLit

Methods

compareF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool Source #

ltF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool Source #

geqF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool Source #

gtF :: forall (x :: k) (y :: k). IndexLit x -> IndexLit y -> Bool Source #

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 Source # showF :: forall (tp :: k). IndexLit tp -> String Source # showsPrecF :: forall (tp :: k). Int -> IndexLit tp -> String -> String Source #
Show (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods showsPrec :: Int -> IndexLit tp -> ShowS Source # show :: IndexLit tp -> String Source # showList :: [IndexLit tp] -> ShowS Source #
Eq (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods (==) :: IndexLit tp -> IndexLit tp -> Bool Source # (/=) :: IndexLit tp -> IndexLit tp -> Bool Source #
Hashable (IndexLit tp) Source # |
Instance details Defined in What4.IndexLit Methods hashWithSalt :: Int -> IndexLit tp -> Int Source # hash :: IndexLit tp -> Int Source #

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