[Agda] Nested with

[Thorsten Altenkirch]

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

My finite universe example (posted last year) contains some examples  
of nested withs.

T.

Begin forwarded message:
> From: Thorsten Altenkirch <txa at Cs.Nott.AC.UK>
> Date: 7 May 2008 16:49:50 BST
> To: agda at lists.chalmers.se
> Subject: a universe of finite types
>
> Hi,
>
> thank you very much for your help!
>
> I thought I might as well post the product of my efforts, showing  
> that the family of finite sets us closed under coproducts, products  
> and exponentials with the associated views. Basically (Simple) Type  
> Theory for Hardware engineers...
>
> For me it was a good way to try out the "with" mechanism which works  
> very nicely (thank you, Ulf). I also realized that our remark in http://www.cs.nott.ac.uk/~txa/publ/ssgp06.pdf 
> , exercise 4 was misleading, you don't need extensionality to  
> implement a view on functions, because this only requires that every  
> code is represented by a function and not the inverse.
>
> I'll have a go and do Sigma and Pi instead: Hardware engineers need  
> dependent types!
>
> Cheers,
> Thorsten
>
>
>


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.

-------------- next part --------------
Skipped content of type multipart/mixed