I don't know enough to understand if the hard troubles described by John
Meacham are real, but I think that even if they are not, the current situation
violates the principle of least surprise for the author of a module.
Such author may be unaware of the need to take special steps to make his
On Sat, Feb 18, 2012 at 15:15, Eugene Crosser cros...@average.org wrote:
I think it would be a right thing to provide the author of an external
module
with baseline C environment by default, compatible with the environment
under
which the modules bundled with the compiler where built. And on
Not sure if I misparsed your response or not.
Its not just things that can or could match the type of the scope, but
basically anything introduced in local scopes around the hole, those can
have types that you can't talk about outside of a local context, due to
existentials that were opened, etc.
For those of us unfamiliar with Agda would somebody explain what you mean by
showing ‘anything introduced in local scopes around the hole’?
If the hole were at the top level then this would be the module context and
loading it into ghci would give you what you need? (Or more realistically you
