| 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
| TestEquality IndexLit Source # | |
Defined in What4.IndexLit Methods testEquality :: forall (a :: k) (b :: k). IndexLit a -> IndexLit b -> Maybe (a :~: b) | |
| HashableF IndexLit Source # | |
Defined in What4.IndexLit Methods hashWithSaltF :: forall (tp :: k). Int -> IndexLit tp -> Int | |
| OrdF IndexLit Source # | |
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 # | |
Defined in What4.IndexLit | |
| Show (IndexLit tp) Source # | |
| Eq (IndexLit tp) Source # | |
| Hashable (IndexLit tp) Source # | |
Defined in What4.IndexLit | |
hashIndexLit :: Int -> IndexLit idx -> Int Source #