What4.Utils.OnlyIntRepr

Defines a GADT for indicating a base type must be an integer. Used for restricting index types in MATLAB arrays.

Documentation

data OnlyIntRepr tp

This provides a GADT instance used to indicate a BaseType must have value BaseIntegerType.

Constructors

tp ~ BaseIntegerType => OnlyIntRepr

Instances

TestEquality OnlyIntRepr

Defined in What4.Utils.OnlyIntRepr

Methods

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

HashableF OnlyIntRepr

Defined in What4.Utils.OnlyIntRepr

Methods

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

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

Hashable (OnlyIntRepr tp)

Defined in What4.Utils.OnlyIntRepr

Methods

hashWithSalt :: Int -> OnlyIntRepr tp -> Int

hash :: OnlyIntRepr tp -> Int

toBaseTypeRepr :: OnlyIntRepr tp -> BaseTypeRepr tp