[Agda] Bezonas helpon !

[Jesper Cockx]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170814/300c589e/attachment-0001.html>