On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh <andres.l...@googlemail.com> wrote: > 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 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
