Accessing definitions in other modules

[LeventErkok]

Currently, any definition that's not in the current module is simply "uninterpreted" when sbvPlugin runs. This is arguably the right behavior as we're not really targeting a whole-program-analysis tool, but rather small local proofs.

But that stops a little short, since even the prelude isn't there. Basic functions such as take, drop etc. are completely gone; even if we can perfectly reason with (at least some) of these.

Of course, the ramifications can be large: Consider filter: If the predicate is symbolic, then we'll choke soon as we merge: There's just no way to handle that currently. But perhaps a happy medium exists?