Not sure if I misparsed your response or not.<div><br></div><div>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. <div>
<br></div><div>The usual agda idiom is to make the hole, then check to see what is available that you can use to build towards filling it in, but those locally introduced things may not have anything in common with the type of the hole.</div>
<div><br></div><div>-Edward</div><div><br></div><div><div class="gmail_quote">On Mon, Feb 13, 2012 at 4:09 AM, Thijs Alkemade <span dir="ltr"><<a href="mailto:thijsalkemade@gmail.com">thijsalkemade@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh <<a href="mailto:andres.loeh@googlemail.com">andres.loeh@googlemail.com</a>> wrote:<br>
> Hi Thijs.<br>
><br>
> Sorry if this has been discussed before.<br>
><br>
> In my opinion, the main advantage of Agda goals is not that the type<br>
> of the hole itself is shown, but that you get information about all<br>
> the locally defined identifiers and their types in the context of the<br>
> hole. Your page doesn't seem to discuss this at all. Without that<br>
> extra info, I don't see much purpose in the feature, though, because<br>
> as others have indicated, it can relatively easily be simulated<br>
> already.<br>
><br>
> Cheers,<br>
> Andres<br>
<br>
</div>Hi Andres,<br>
<br>
Thanks for your feedback. Showing everything in scope that matches or<br>
can match the type of a hole is certainly something I am interested<br>
in, but I'm afraid it's out of the scope of this project. I think<br>
finding the types of the holes is a good first step that should make<br>
this feature easier to implement later.<br>
<br>
Best regards,<br>
<font color="#888888">Thijs Alkemade<br>
</font><div><div></div><div class="h5"><br>
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
</div></div></blockquote></div><br></div></div>