On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh
Hi Thijs.
Sorry if this has been discussed before.
In my opinion, the main advantage of Agda goals is not that the type of the hole itself is shown, but that you get information about all the locally defined identifiers and their types in the context of the hole. Your page doesn't seem to discuss this at all. Without that extra info, I don't see much purpose in the feature, though, because as others have indicated, it can relatively easily be simulated already.
Cheers, Andres
Hi Andres, Thanks for your feedback. Showing everything in scope that matches or can match the type of a hole is certainly something I am interested in, but I'm afraid it's out of the scope of this project. I think finding the types of the holes is a good first step that should make this feature easier to implement later. Best regards, Thijs Alkemade