[Agda] question on `with'

[Wolfram Kahl]

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