[Agda] Nested with

[Nils Anders Danielsson]

On 2009-06-05 02:09, Ben Horsfall wrote:
> Could someone post/direct me to an example of a nested with-expression?

There are nested uses of with in the following standard library modules:

  http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Bin.html
  http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.Dec.html
  http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.Properties.html
  http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Nat.Coprimality.html
  http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Nat.GCD.html
  http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Nat.LCM.html
  http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Vec.html

See the function Data.Vec.group, for instance.

-- 
/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.