[Agda] Agda and machine learning

mechvel at scico.botik.ru mechvel at scico.botik.ru
Thu Sep 24 18:15:11 CEST 2020


On 2020-09-24 16:15, mechvel at scico.botik.ru wrote:
>> [..]

> (1) A very simple problems. For example, to prove  reverse (reverse xs) 
> == xs
>     for a list xs,
>     or to prove that _*_ in unary system for natural numbers is 
> commutative
>     (m * n == n * n).
> [..]

Fixing a typo: this should be  (m * n == n * m).

--
SM


More information about the Agda mailing list