[Agda] new generalize feature, first version

[Peter Divianszky]

It's great that you like this feature.

My motivation was that now I am working with Ambrus Kaposi on 
type-theory-in-type-theory, and I have to formalize his work in Agda.

A little part of the basics, without and with forall-generalization (the 
second covers more type formers):

https://bitbucket.org/akaposi/tt-in-tt/src/6f71db610e9d27147abcf743cbe1731ed5c9ca0a/TTR.agda?at=master&fileviewer=file-view-default

https://github.com/divipp/agda/blob/master/test/Succeed/Generalize.agda

If you look at the type of ,∘ for example, you will notice the difference.

By the way, I fixed an error in the implementation and now all Agda 
tests are OK including the new one.

These tasks are also ready now:

- automatic generalization of record fields and constructor types
- allow 'generalize' keyword in submodules

Best,
Peter


On 2018-03-29 19:39, Robby Findler 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
>