[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