[Agda] Needs doing

[NISHIHARA Hideaki]

Hello,

On Thu, 03 Feb 2005 15:29:56 +0100
Ana Bove <bove at cs.chalmers.se> wrote:
> I 
> think it is very important to have a reasonable user manual/tutorial for 
> Agda by that time. It should be something for beginners, maybe even 
> beginner in the use of proof assistant. I don't really know if the 
> documentation Makoto's team is writing could be use for that purpose. 
> Sometimes a documentation goes more into details and it is aim more to 
> experts.

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?


Hideaki, NISHIHARA
Reseach Center for Verification and Semantics, AIST, Japan