Copyright | (c) Galois Inc. 2020 |
---|---|
License | BSD3 |
Maintainer | Joe Hendrix <jhendrix@galois.com> |
Safe Haskell | None |
Language | Haskell2010 |
Defines a GADT for indicating a base type must be a natural number. Used for restricting index types in MATLAB arrays.
Synopsis
- data OnlyNatRepr tp = tp ~ BaseNatType => OnlyNatRepr
- toBaseTypeRepr :: OnlyNatRepr tp -> BaseTypeRepr tp
Documentation
data OnlyNatRepr tp Source #
This provides a GADT instance used to indicate a BaseType
must have
value BaseNatType
.
tp ~ BaseNatType => OnlyNatRepr |
Instances
TestEquality OnlyNatRepr Source # | |
Defined in What4.Utils.OnlyNatRepr testEquality :: OnlyNatRepr a -> OnlyNatRepr b -> Maybe (a :~: b) # | |
HashableF OnlyNatRepr Source # | |
Defined in What4.Utils.OnlyNatRepr hashWithSaltF :: Int -> OnlyNatRepr tp -> Int # hashF :: OnlyNatRepr tp -> Int # | |
Hashable (OnlyNatRepr tp) Source # | |
Defined in What4.Utils.OnlyNatRepr hashWithSalt :: Int -> OnlyNatRepr tp -> Int # hash :: OnlyNatRepr tp -> Int # |
toBaseTypeRepr :: OnlyNatRepr tp -> BaseTypeRepr tp Source #