[Agda] Bool P -> Dec P'

[Ulf Norell]

On Fri, Dec 6, 2013 at 12:00 PM, Sergei Meshveliani <mechvel at botik.ru>wrote:

> Please, how to write this via `case' ?
>
> This is the conversion of a Boolean predicate to the decidable one:
>
> ----------------------------------------------------------------------
> open import Data.Unit         using (⊤)
> open import Data.Bool as Bool using (Bool; true; false; T)
>
> boolP→Dec : ∀ {α} {A : Set α} → (P : A → Bool) → let P' : A → Set
>                                                      P' = T ∘ P
>                                                  in  Decidable P'
> boolP→Dec P x  with  P x
> ...          | true  = yes ⊤.tt
> ...          | false = no λ()
> ----------------------------------------------------------------------
>
> How to rewrite this via `case', so that it is type-checked ?
> (in development Agda of November 2013).
>

boolP→Dec : ∀ {α} {A : Set α} → (P : A → Bool) → Decidable (T ∘ P)
boolP→Dec P x =
  case P x return Dec ∘ T of λ
  { true  → yes _
  ; false → no λ()
  }

You need to use case_return_of_ since it's a dependent pattern match (the
type of the branches are different).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131206/0d879fc3/attachment.html