[Agda] AIM5

[Peter Dybjer]

While in Japan we discussed when to have AIM5 with Makoto and Yoshiki and decided tentatively on the week 25-29 September in Göteborg.

The following list of possible CodeSprint topics was compiled.

    - Termination & positivity checker
    - Proof General Kit adaptation
           (not on the mainline Agda2 system functionality development)
    - Agate2 compiler (non-mainline)
    - Pattern refinment interaction
    - Translator to Core language (non-mainline)
    - Inductive Family, Pi in Set, signuature, singleton type, ...
    - User defined reduction with justification
    - Better hidden argument inference for Setoid etc.
    - Epigram layer on top of Agda2

Peter