[Agda] question on `with'

[Sergei Meshveliani]

Thank you. 
I knew about `inspect'. And I have succeeded with `inspect' in the
original example (which is a bit more complex).

But I have not any general clear understanding about usage of `inspect'.
This feature somehow does not look nice, is difficult for intuition.
At least, it is very desirable to have its explanation in the Reference
Manual on the language.

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

------
Sergei



On Thu, 2016-08-25 at 11:19 -0400, Wolfram Kahl wrote:
> Hi Sergei,
> 
>   just a guess:
> 
> On Thu, Aug 25, 2016 at 06:51:22PM +0400, Sergei Meshveliani wrote:
> > Please, what is wrong in the following program?
> > 
> > -------------------------------------------------------------------------
> > open import Data.Bool        using (Bool; true; false; _≟_)
> > open import Data.Nat         using (ℕ)
> > open import Relation.Nullary using (yes; no)
> > open import Relation.Binary.PropositionalEquality using (_≡_)
> 
>                                                               , inspect
> > 
> > 
> > f :  (P : ℕ → Bool) → ℕ → ℕ
> > f P x
> >     with  P x | P x ≟ false
>       with  P x | inspect P x | P x ≟ false
> 
> > 
> > ... | _ | yes eq =  0
>   ... | px | [ Px≡ps ] | yes eq = ...
> 
> And now you could try subst or rewrite with Px≡ps
> 
> 
> (Haven't actually tried this.)
> 
> 
> Wolfram
>