No, the kata is already using prod in the library. I just introduced an alternative notation # to avoid conflicts with * which is mainly used for natural-number multiplication. If you switch all of #s in your definitions and proofs to *s (the library's notation for prod type), you will notice that most of the code will still work, except at some places where Coq is confused between prod (notation for type) and mul (notation for nat).

I don't think the tarai relation correctly reflects the tarai function given. Shouldn't the arguments be rotated?

Published the fixed version.

I have a fixed version ready. I can't update the code right now because there's server error.

In short, the updates are:

• [[ e ]] instead of [ e ]
• ==> ==>* ~~>*T ~~>*F instead of => =>* ~>*T ~>*F

Approved :)

Approved :)

Approved :)

Approved :)

Approved :)

Thanks for the info. Changed the description and tests.

Fixed.

Fixed.