[Agda] Needs doing

[Peter G. Hancock]

>>>>> NISHIHARA Hideaki wrote (on Mon, 07 Feb 2005 at 09:08):

    > I also think reasonable documents on Agda are needed, and in AIST we
    > are writing such documents.  Last December, an Agda beginner read
    > our tutorial and told us that he could not understand Agda.
    > So we discussed again the contents of our tutorial, and we are
    > writing a new version.  We believe it is good for beginners.

    > We plan two documents now:
    > * tutorial for beginners,
    > * Agda reference manual.
    > I think Agda library manual and two documents above will cover
    > all Agda users.

    > Now I have a question.  Which version of Agda should we use to
    > write documents?  Should we mention about hidden arguments,
    > literals, etc. in a tutorial?

I am sorry to be so late in responding.

I hope very much that you will explain hidden arguments, "literals"
(I have no idea what they are) and so on.  But only after the basic,
unfancy Agda has been explained.  Perhaps each of these things could
be confined to its own (high-numbered) chapter/appendix?

Peter Hancock