[Agda] Beginner's Troubles With Documentation

Vag Vagoff vag.vagoff at gmail.com
Thu Sep 17 11:56:37 CEST 2009


Hi!

I'm a tabula rasa beginner so I hope my troubles will help to improve 
documentation. I've encountered a few unanswered questions after reading 
tons of documentation on Agda2:

1. What is exact meaning of forall keyword?
2. How data and codata might be expressed in UTT_e?
3. What exact and complete explanation of difference between type 
parameters and type indices and how to express parameters in UTT_e?
4. Why @ reserved? I haven't found where @ mentioned in documentation at all
5. Why open and import separated into two language constructions instead 
of one as in many other languages?

Please, explain or direct me to the place where answers lie.

Thanks in advance.



More information about the Agda mailing list