[Agda] Documentation on "with" patterns

[Roly Perera]

Thanks for both of the replies to my question.  I'll get stuck in.

[I'm surprised at how easy it is (for someone with no real DTT
background) to get up to speed with Agda...having experience in
Haskell certainly helps!]

2009/9/19 Liang-Ting Chen <xcycl at iis.sinica.edu.tw>:
> You may also read the paper "The View From Left" by Conor McBride for deeper
> understanding.
>
> On Sat, Sep 19, 2009 at 4:38 AM, Nils Anders Danielsson <nad at cs.nott.ac.uk>
> wrote:
>>
>> On 2009-09-18 15:03, Roly Perera wrote:
>>>>
>>>> Is there any documentation which explains how the Agda "with"
>>>> pattern-matchign notation is used?
>>
>> You can have a look at Ulf Norell's tutorial "Dependently Typed
>> Programming in Agda", or Ulf's thesis. The wiki links to both.