[Agda] Bezonas helpon !

[Ulf Norell]

The fact that foldr₁ is using a private recursive helper function will
likely make it impossible to prove your theorem.

/ Ulf

On Mon, Aug 14, 2017 at 6:47 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> Maybe you can explain what approaches you have already tried and why you
> got stuck? I think people would be more inclined to help that way.
>
> To get you started on proof1, here's a hint: since you are proving
> something about the functions foldr₁ and _⊔_, you can take a look at their
> definitions and follow the same structure for your proof. For example,
> since foldr₁ is defined in terms of the helper function foldr, you probably
> also need to define a helper lemma that proves a similar statement about
> foldr.
>
> Best regards,
> Jesper
>
> 2017-08-14 18:33 GMT+02:00 Serge Leblanc <33dbqnxpy7if at gmail.com>:
>
>> Saluton, neniu bonvolas helpi min?
>>
>> Hi, nobody wants to help me?
>>
>> On 2017-08-06 18:23, Serge Leblanc wrote:
>>
>> Dear All,
>> I need help to finish these lemmas.
>> They have the same meaning, I am right?
>> All helpers are welcome!
>>
>> Estimata ĉiuj,
>> Mi bezonas helpon por daŭrigi ci-tiuj pruvojn!
>> Ĉu ili havas je la saman signifon! Ĉu mi pravas?
>> Ĉiuj helpantoj estas bonvenaj!
>>
>> Sincere.
>> --
>> Serge Leblanc
>> ------------------------------
>> gpg --search-keys 0x67B17A3F
>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>>
>>
>> --
>> Serge Leblanc
>> ------------------------------
>> gpg --search-keys 0x67B17A3F
>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
> _______________________________________________
> 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/20170814/a61702e8/attachment.html>