[Agda] Agda documentation

[Jon Sterling]

This is exciting! I really look forward to seeing something about sized
types, and also irrelevance. What I've seen so far looks great so far.

Thanks,
Jon


On Thu, Nov 5, 2015, at 06:41 AM, Harley Eades III wrote:
> Hi, everyone.
> 
> I couldn’t agree more with what everyone is saying.  Documentation will
> go a
> long way for Agda!  This is very exciting.
> 
> Andy, I often feel the exact same way.
> 
> Very best,
> Harley
> 
> > On Nov 5, 2015, at 8:59 AM, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:
> > 
> > On 5 November 2015 at 12:24, Ulf Norell <ulf.norell at gmail.com> wrote:
> >> In case you're not following the github repository closely, you might not
> >> know about the documentation project that is slowly taking shape at
> >> http://agda.readthedocs.org. I just added a section on with-abstraction that
> >> might be of interest to people:
> >> 
> >> http://agda.readthedocs.org/en/latest/language/with-abstraction.html
> > 
> > That looks really useful. If the rest of the documentation ends up
> > being that good, it will be GREAT!. Agda has many wonderful features,
> > but finding out about some of them at the moment is like playing a
> > text adventure game in an emacs buffer! (I pick up sized types and see
> > what I can do with them, emacs responds with some sometimes cryptic
> > comment, I pick up something else, etc, etc -- you get the idea.)
> > 
> > Andy
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda