[Agda] join 2 `with'|

Sergei Meshveliani mechvel at botik.ru
Wed Nov 5 09:21:34 CET 2014


On Tue, 2014-11-04 at 16:43 -0600, Christopher Jenkins wrote:
> 
> [..]
> I have actually been thinking about writing a blog post targeted at
> newbies (such as myself) on the sometimes unintuitive behaviour of
> `with' (and in particular, `rewrite'). Should anyone be interested I
> can send a link on this email chain once I have written it.
> 

Thank you. Send me a link, please.

Also it will be nice to have a kind of a  draft manual  (describing
several pitfalls) on using `with', `case_of', `case_return_of'.

------
Sergei





More information about the Agda mailing list