sbv-8.12: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

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

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)