[Agda] question on `with'
Sergei Meshveliani
mechvel at botik.ru
Thu Aug 25 20:08:00 CEST 2016
On Thu, 2016-08-25 at 18:47 +0200, Ulf Norell wrote:
>
>
> 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
I see now, thank you. It is is the section of With-abstraction in
Manual.
In the old manual there was the Keywords section. With `keywords' it is
easier to find things.
------
Sergei
More information about the Agda
mailing list