I downloaded and compiled Agda2 today. And I'm having fun playing with it and trying out the examples. But I find it a little disappointing that many of the example files are syntactically incorrect. I suggest that those examples are either fixed or removed. Having wrong examples can be confusing for a beginner. -- Lennart