[Agda] First-Class Type Issue

[Ulf Norell]

The problem is that the `case_of_` function is non-dependent (the type of
the branches cannot depend of the value you case on).
You can use `case_return_of_` instead if you need a dependent match:

getStringOrInt : (x : Bool) → StringOrInt x
getStringOrInt x = case x return StringOrInt of λ where
  true → 94
  false → "Ninety Four"

However, the "correct" way to write the function is

getStringOrInt : (x : Bool) → StringOrInt x
getStringOrInt true = 94
getStringOrInt false = "Ninety Four"

/ Ulf

On Thu, Apr 16, 2020 at 8:35 AM Philippe de Rochambeau <phiroc at free.fr>
wrote:

> Hello,
>
> when I load the following module,
>
> open import Agda.Builtin.Bool
> open import Agda.Builtin.Nat
> open import Agda.Builtin.String
> open import Function using (case_of_)
>
> StringOrInt : (x : Bool) → Set
> StringOrInt x  = case x of λ where
>     true → Nat
>     false → String
>
> getStringOrInt : (x : Bool) → StringOrInt x
> getStringOrInt x = case x of λ where
>   true → 94
>   false → "Ninety Four"
>
>
> … I get this error message:
>
> String != Nat
> when checking that the expression "Ninety Four" has type Nat
>
> Do lambdas only return one data type (in this case, Nat)?
>
> Cheers,
>
> Philippe
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200416/55a1287e/attachment.html>