Content deleted Content added
Removed {{context}} warning and changed a bit the introduction |
→Agda 2: added Makoto as emacs mode developer |
||
Line 9:
The second version of Agda, Agda 2, is currently being developed at [[Chalmers_University_of_Technology|Chalmers]] by Ulf Norell. The syntax has completely changed from Agda 1 (though some conversion tools are being developed as well), introducing for instance implicit variables, that can be omitted when deduceable from the context. Agda 2 also makes an intensive use of [[Unicode]] as a way to obtain easily-readable proofs.
Agda 2 provides either a commandline tool or a powerful [[emacs]] mode, developed by Makoto Takeyama and Nils Anders Danielsson.
The 6th Agda Implementor's Meeting was held in [[Göteborg]] in May 2007. AIM7 is scheduled for november in [[Osaka]] and should focus on the transition from Agda 1 to Agda 2.
| |||