[Agda] Documentation on "with" patterns

[Liang-Ting Chen]

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.
>
> --
> /NAD
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses, which could damage your computer
> system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
sincerely,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090919/21871b53/attachment-0001.html