what4-1.0: 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

NatIndexLit :: !Natural -> IndexLit BaseNatType 
BVIndexLit :: 1 <= w => !(NatRepr w) -> !(BV w) -> IndexLit (BaseBVType w) 
Instances
TestEquality IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

testEquality :: IndexLit a -> IndexLit b -> Maybe (a :~: b) #

OrdF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

compareF :: IndexLit x -> IndexLit y -> OrderingF x y #

leqF :: IndexLit x -> IndexLit y -> Bool #

ltF :: IndexLit x -> IndexLit y -> Bool #

geqF :: IndexLit x -> IndexLit y -> Bool #

gtF :: IndexLit x -> IndexLit y -> Bool #

ShowF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

withShow :: p IndexLit -> q tp -> (Show (IndexLit tp) -> a) -> a #

showF :: IndexLit tp -> String #

showsPrecF :: Int -> IndexLit tp -> String -> String #

HashableF IndexLit Source # 
Instance details

Defined in What4.IndexLit

Methods

hashWithSaltF :: Int -> IndexLit tp -> Int #

hashF :: 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 #