What4.IndexLit

Documentation

data IndexLit idx where

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

Defined in What4.IndexLit

Methods

testEquality :: forall (a :: k) (b :: k). IndexLit a -> IndexLit b -> Maybe (a :~: b)

OrdF IndexLit

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

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

Defined in What4.IndexLit

Methods

hashWithSaltF :: forall (tp :: k). Int -> IndexLit tp -> Int

hashF :: forall (tp :: k). IndexLit tp -> Int

Eq (IndexLit tp)

Defined in What4.IndexLit

Methods

(==) :: IndexLit tp -> IndexLit tp -> Bool

(/=) :: IndexLit tp -> IndexLit tp -> Bool

Show (IndexLit tp)

Defined in What4.IndexLit

Methods

showsPrec :: Int -> IndexLit tp -> ShowS

show :: IndexLit tp -> String

showList :: [IndexLit tp] -> ShowS

Hashable (IndexLit tp)

Defined in What4.IndexLit

Methods

hashWithSalt :: Int -> IndexLit tp -> Int

hash :: IndexLit tp -> Int

hashIndexLit :: Int -> IndexLit idx -> Int