[Agda] proofs with "with"

[Christopher Jenkins]

 I hate to advertise for myself twice on the mailing list, but I am
currently working on a series of blog posts + videos for Agda beginners,
starting with common uses and pitfalls of "with" for functions and proofs.
The very next topic I have planned is how to use "inspect", using as an
example the filter function on lists and a proof that all elements of a
filtered lists satisfy the predicate used. I plan on doing these tomorrow,
and you can find them then from the following links:

Vidya:
https://www.youtube.com/playlist?list=PLWU5W_m7Gj8-CRDXAzQThCf8MSq7wYdff
(will be titled "with: intro(in)spection")
Blag: http://serendependy.blogspot.com/ (same title)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141215/8771014a/attachment-0001.html