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

Copyright | (c) Galois Inc. 2020
License | BSD3
Maintainer | Joe Hendrix <jhendrix@galois.com>
Safe Haskell | Safe-Inferred
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 = tp ~ BaseIntegerType => OnlyIntRepr
- toBaseTypeRepr :: OnlyIntRepr tp -> BaseTypeRepr tp

# Documentation

data OnlyIntRepr tp 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 :: k) (b :: k). OnlyIntRepr a -> OnlyIntRepr b -> Maybe (a :~: b) Source #
HashableF OnlyIntRepr Source # |
Instance details Defined in What4.Utils.OnlyIntRepr Methods hashWithSaltF :: forall (tp :: k). Int -> OnlyIntRepr tp -> Int Source # hashF :: forall (tp :: k). 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 :: OnlyIntRepr tp -> BaseTypeRepr tp Source #