We currently don't support arrays created in lambda functions; nor functions that take/return arrays. Not sure how useful this is, but might be nice. Note that we can't simply "recognize and error" for these, as lambda-array is a valid construct used internally. (see Documentation.SBV.Examples.Misc.LambdaArray for an example.) That is, it's perfectly fine to refer to a top-level array created in a lambda, as that function will make sense in the context of the definition. What we should doing is rejecting it if only called from sbv2smt; but we don't really have a good way to distinguish that for the time being.
We currently don't support arrays created in lambda functions; nor functions that take/return arrays. Not sure how useful this is, but might be nice. Note that we can't simply "recognize and error" for these, as lambda-array is a valid construct used internally. (see
Documentation.SBV.Examples.Misc.LambdaArrayfor an example.) That is, it's perfectly fine to refer to a top-level array created in a lambda, as that function will make sense in the context of the definition. What we should doing is rejecting it if only called fromsbv2smt; but we don't really have a good way to distinguish that for the time being.Examples that currently aren't supported: