What4.IndexLit

Documentation

data IndexLit idx where

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

Defined in What4.IndexLit

Methods

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

OrdF IndexLit

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

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

Defined in What4.IndexLit

Methods

hashWithSaltF :: Int -> IndexLit tp -> Int

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