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

Copyright(c) Galois Inc. 2020
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.Utils.OnlyNatRepr

Description

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

Synopsis

Documentation

data OnlyNatRepr tp Source #

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

Constructors

tp ~ BaseNatType => OnlyNatRepr 
Instances
TestEquality OnlyNatRepr Source # 
Instance details

Defined in What4.Utils.OnlyNatRepr

Methods

testEquality :: OnlyNatRepr a -> OnlyNatRepr b -> Maybe (a :~: b) #

HashableF OnlyNatRepr Source # 
Instance details

Defined in What4.Utils.OnlyNatRepr

Methods

hashWithSaltF :: Int -> OnlyNatRepr tp -> Int #

hashF :: OnlyNatRepr tp -> Int #

Hashable (OnlyNatRepr tp) Source # 
Instance details

Defined in What4.Utils.OnlyNatRepr

Methods

hashWithSalt :: Int -> OnlyNatRepr tp -> Int #

hash :: OnlyNatRepr tp -> Int #