[Agda] pattern matching order

[Thorsten Altenkirch]

Thank you, Andreas.

Wouldn’t it be possible to have a flag to say wether one wants the old
behaviour or the new one?

Cheers,
Thorsten

On 03/04/2017, 15:21, "Agda on behalf of Andreas Abel"
<agda-bounces at lists.chalmers.se on behalf of abela at chalmers.se> wrote:

>Hi Thorsten,
>
>this is this issue #408
>
>   https://github.com/agda/agda/issues/408
>
>You can read there that I implemented a split strategy that would make
>your code work, but did not activate it, since fixes the split strategy
>to an extend where changing the order of clauses could not give you the
>other behavior.  In particular, it was not backwards-compatible.
>Whether we should turn on the new split strategy is still undecided
>(since 2012).
>
>However, now you can use the --exact-split flag to let Agda alert you
>when your clauses do not lead to definitional equalities.
>
>Cheers,
>Andreas
>
>On 03.04.2017 15:08, Thorsten Altenkirch wrote:
>> Hi,
>>
>> I tried to define the following function by pattern matching
>>
>> codeDouble : ∀{n : ℕ} → Bool × Fin n → Fin (double n)
>> codeDouble {zero} (b , ())
>> codeDouble {suc n} (false , zero) = zero
>> codeDouble {suc n} (true , zero) = suc zero
>> codeDouble {suc n} (b , suc x) = suc (suc (codeDouble (b , x)) )
>>
>> But to my confusion the term "codeDouble {suc n} (b , suc x) “ didn’t
>> reduce. This can be fixed by changing the order
>>
>> codeDouble : ∀{n : ℕ} → Bool × Fin n → Fin (double n)
>> codeDouble {zero} (b , ())
>> codeDouble {suc n} (b , suc x) = suc (suc (codeDouble (b , x)) )
>> codeDouble {suc n} (false , zero) = zero
>> codeDouble {suc n} (true , zero) = suc zero
>>
>> I guess I can answer this myself: since I first match on the boolean
>> agda decides also to do case analysis first on the boolean and then on
>> the Fin which duplicates my last line and has the effect that the
>> defining equality doesn’t hold definitionally (this is always a bit
>> agda). In this case agda could have matched my definition by changing
>> the order. Is this too much to ask for?
>>
>> Cheers,
>> Thorsten
>>
>>
>>
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please send it back to me, and immediately delete it.
>>
>> Please do not use, copy or disclose the information contained in this
>> message or in any attachment.  Any views or opinions expressed by the
>> author of this email do not necessarily reflect the views of the
>> University of Nottingham.
>>
>> This message has been checked for viruses but the contents of an
>> attachment may still contain software viruses which could damage your
>> computer system, you are advised to perform your own checks. Email
>> communications with the University of Nottingham may be monitored as
>> permitted by UK legislation.
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
>-- 
>Andreas Abel  <><      Du bist der geliebte Mensch.
>
>Department of Computer Science and Engineering
>Chalmers and Gothenburg University, Sweden
>
>andreas.abel at gu.se
>http://www.cse.chalmers.se/~abela/
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.