[Agda] new generalize feature, first version

[Apostolis Xekoukoulotakis]

I agree with Nils points,

i think that it is better to return an error if you try to generalize a
name that already exists.

In idris, where every implicit argument is generalized, you get into
problems because of that.
You want your function to get a specific value, but instead it assumes that
it is an implicit argument.

http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#using-notation
(Check the "important section" there)

So, if it returns an error in such a case and since generalization are
local, this might work.

On Thu, Mar 29, 2018 at 8:39 PM, Robby Findler <robby at eecs.northwestern.edu>
wrote:

> On Thu, Mar 29, 2018 at 12:24 PM, Thorsten Altenkirch
> <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> > I like it too. Also one wouldn't need to doctor agda code anymore to
> make it publishable (destroying the literate idea in the process).
>
> Yay! "Run your research" support in Agda! I love it.
>
> More generally, while I'm a total newbie compared to most people here,
> I really do love the design of Agda. It is so ... I don't have a good
> word for it ... *human*. I love the idea that it gets features that
> make it easier to show sensible and yet accurate code snippets in
> papers.
>
> Robby
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180330/677f7105/attachment.html>