what4-1.3: Solver-agnostic symbolic values support for issuing queries
Safe HaskellNone
LanguageHaskell2010

What4.IndexLit

Synopsis

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 #