What4.Utils.OnlyNatRepr

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

Documentation

data OnlyNatRepr tp

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

Constructors

tp ~ BaseNatType => OnlyNatRepr

Instances

TestEquality OnlyNatRepr

Defined in What4.Utils.OnlyNatRepr

Methods

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

HashableF OnlyNatRepr

Defined in What4.Utils.OnlyNatRepr

Methods

hashWithSaltF :: Int -> OnlyNatRepr tp -> Int

hashF :: OnlyNatRepr tp -> Int

Hashable (OnlyNatRepr tp)

Defined in What4.Utils.OnlyNatRepr

Methods

hashWithSalt :: Int -> OnlyNatRepr tp -> Int

hash :: OnlyNatRepr tp -> Int

toBaseTypeRepr :: OnlyNatRepr tp -> BaseTypeRepr tp