Documentation.SBV.Examples.Misc.NestedArray

Demonstrates how to model nested-arrays, i.e., arrays of arrays in SBV. Instead of SMTLib's nested model, in SBV we use a tuple as an index, which is isomorphic to nested arrays.

Documentation

nestedArray :: IO (Integer, Integer)

Model a nested array that is indexed by integers, and we store another integer to integer array in each index. We have:

>>> nestedArray
(2,10)