[Agda] First-Class Type Issue

[Philippe de Rochambeau]

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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200416/89fd06ff/attachment.html>