[Agda] Documentation on "with" patterns

[Nils Anders Danielsson]

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.