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
TestEquality IndexLit Source # | |
Defined in What4.IndexLit | |
HashableF IndexLit Source # | |
Defined in What4.IndexLit | |
OrdF IndexLit Source # | |
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 # | |
Show (IndexLit tp) Source # | |
Eq (IndexLit tp) Source # | |
Hashable (IndexLit tp) Source # | |
Defined in What4.IndexLit |
hashIndexLit :: forall (idx :: BaseType). Int -> IndexLit idx -> Int Source #