[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