[Agda] with -> case example

[Andreas Abel]

I'd guess this is a classic application of ``with'', so using ``case'' 
gives no advantage here...

On 08.12.2013 10:10, Sergei Meshveliani wrote:
> Please, how to rewrite this to `case' ?
>
>
> filterStep : ∀ {α} {A : Set α}
>               (p : A → Bool) → (x : A) → p x ≡ true → (xs : List A) →
>                                     filter p (x ∷ xs) ≡ x ∷ (filter p xs)
> filterStep p x px=T xs
>                         with  p x | px=T
> ...                  | .true | PE.refl = PE.refl
>
>
> -------------------------------------------------------------------------
> filterStep p x px=T xs =  case (p x , px=T)  of \
>                                           { (.true , PE.refl) → PE.refl }
> " p x != true of type Bool
>    when checking that the expression px=T has type true ≡ true
> "
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>