sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Documentation.SBV.Examples.Misc.NestedArray

Description

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.

Synopsis

- nestedArray :: IO (Integer, Integer)

# Documentation

nestedArray :: IO (Integer, Integer) Source #

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

    >>> nestedArray
    (0,10)