[Agda] question on `with'

[Ulf Norell]

On Thu, Aug 25, 2016 at 6:31 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

>
> I do not find `inspect' and `rewrite' there.
> Who knows, please, are they in the manual?
>

http://agda.readthedocs.io/en/latest/language/with-abstraction.html#rewrite
http://agda.readthedocs.io/en/latest/language/with-abstraction.html#the-inspect-idiom

You might find the entire section on with-abstraction instructive.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160825/3b03edee/attachment.html