[Agda] question on `with'

[Sergei Meshveliani]

On Thu, 2016-08-25 at 18:33 +0300, Roman wrote:
> You matched on `P x` with a wildcard pattern, Agda introduced a dummy
> variable `w` for it and rewrote `P x`  to `w` everywhere in the
> context, hence the type of `eq` is `w ≡ false`.
> 

But

  f P x  with  P x | P x ≟ false

  ... | false | yes eq =  0
                           where debug : P x ≡ false
                                 debug = eq
  ... | _ | _ =  1

is not type-checked neither.





> Here is how you can make it work:
> 
> 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 (_≡_)
> 
> 
> f :  (P : ℕ → Bool) → ℕ → ℕ
> f P x
>     with  P x | P x ≟ false
> 
> ... | p | yes eq =  0
>                     where debug : p ≡ false
>                           debug = eq
> ... | _ | _ =  1
>