| Copyright | (c) Galois Inc. 2020 |
|---|---|
| License | BSD3 |
| Maintainer | Joe Hendrix <[email protected]> |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Utils.OnlyIntRepr
Description
Defines a GADT for indicating a base type must be an integer. Used for restricting index types in MATLAB arrays.
Synopsis
- data OnlyIntRepr (tp :: BaseType) = tp ~ BaseIntegerType => OnlyIntRepr
- toBaseTypeRepr :: forall (tp :: BaseType). OnlyIntRepr tp -> BaseTypeRepr tp
Documentation
data OnlyIntRepr (tp :: BaseType) Source #
This provides a GADT instance used to indicate a BaseType must have
value BaseIntegerType.
Constructors
| tp ~ BaseIntegerType => OnlyIntRepr |
Instances
| TestEquality OnlyIntRepr Source # | |
Defined in What4.Utils.OnlyIntRepr Methods testEquality :: forall (a :: BaseType) (b :: BaseType). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) # | |
| HashableF OnlyIntRepr Source # | |
Defined in What4.Utils.OnlyIntRepr Methods hashWithSaltF :: forall (tp :: BaseType). Int -> OnlyIntRepr tp -> Int # hashF :: forall (tp :: BaseType). OnlyIntRepr tp -> Int # | |
| Eq (OnlyIntRepr tp) Source # | |
Defined in What4.Utils.OnlyIntRepr Methods (==) :: OnlyIntRepr tp -> OnlyIntRepr tp -> Bool # (/=) :: OnlyIntRepr tp -> OnlyIntRepr tp -> Bool # | |
| Hashable (OnlyIntRepr tp) Source # | |
Defined in What4.Utils.OnlyIntRepr | |
toBaseTypeRepr :: forall (tp :: BaseType). OnlyIntRepr tp -> BaseTypeRepr tp Source #