what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc. 2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
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

Instances details

TestEquality OnlyIntRepr Source # |
Instance details Defined in What4.Utils.OnlyIntRepr Methods testEquality :: forall (a :: BaseType) (b :: BaseType). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) Source #
HashableF OnlyIntRepr Source # |
Instance details Defined in What4.Utils.OnlyIntRepr Methods hashWithSaltF :: forall (tp :: BaseType). Int -> OnlyIntRepr tp -> Int Source # hashF :: forall (tp :: BaseType). OnlyIntRepr tp -> Int Source #
Eq (OnlyIntRepr tp) Source # |
Instance details Defined in What4.Utils.OnlyIntRepr Methods (==) :: OnlyIntRepr tp -> OnlyIntRepr tp -> Bool Source # (/=) :: OnlyIntRepr tp -> OnlyIntRepr tp -> Bool Source #
Hashable (OnlyIntRepr tp) Source # |
Instance details Defined in What4.Utils.OnlyIntRepr Methods hashWithSalt :: Int -> OnlyIntRepr tp -> Int Source # hash :: OnlyIntRepr tp -> Int Source #

toBaseTypeRepr :: forall (tp :: BaseType). OnlyIntRepr tp -> BaseTypeRepr tp Source #