[Agda] Possible bug

[Ulf Norell]

On Fri, May 9, 2008 at 10:31 AM, Chris Eidhof <chris at eidhof.nl> wrote:

> Hey everyone,
>
> This morning, we were experimenting with Agda, and we think we might have
> found a possible bug. Hopefully this is not a bug, but then I am very
> interested in the explanation of this behavior. This is our program:
>
>  module Test where
>>
>> open import Data.String
>> open import Data.Bool
>> open import Data.List
>>
>> test : String -> Bool
>> test xs with toList xs
>> ... | [] = false
>> ... | ys = true
>>
>
> If we now evaluate 'test ""' it return false, but 'test "hi"' also returns
> false. I would expect the last case to return true. If we replace the ys by
> (y ∷ ys) it does work.


I get test "hi" reducing to true as expected. Did you get the latest Agda
version from darcs? It might be that it's an old bug that has already been
fixed.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080509/bc9d1b73/attachment.html