The tests for my .check() function give:

SyntaxError: Unexpected token u in JSON at position 0
    at JSON.parse (<anonymous>)
    at Context.<anonymous> (test.js:47:35)

My code doesn't mention JSON, nor does the problem specification say "keys must not crash when attempting to json serialize them"

How exactly do those solutions work? What does codewars interpret a top-level return in a javascript solution as?

I think fixed in https://www.codewars.com/kumite/5ee9ba7eb44cc3000fcd6bb1?sel=5eec704497084e002874c861?

The fix is to replace the word CompareOp with Compare in the tests. I tried to fix it, but I'm finding it really hard to work out how to edit a kata translation.

Fixed

ah, i see the issue, typo in an ast node name.

didn't my update above fix that?

Lean translation: https://www.codewars.com/kumite/5eeb6edee8db87001c07b721?sel=5eeb6edee8db87001c07b721

This seems to match https://www.codewars.com/kata/5ea9b14c9b7bf50001b88e55 too.

Do you have a link to a kata using SUBMISSION?

Fixed in https://www.codewars.com/kumite/5ee8cf1b16e9820028c08c2c?sel=5ee9ba7eb44cc3000fcd6bb1, mind approving?

Whoops, that should probably be forbidden!

i don't see your solution?

Just updated the description to not clobber the Coq one - I was not aware the description was shared.

My approach here is copied from the one used by https://www.codewars.com/kata/5e90c3814af7f4002e2535af.

I agree I've seen the SUBMISSION pattern too, but I didn't have an example to hand to copy from.

And checking that user solution has type SUBMISSION in tests.

I believe this is covered by the (@nat_is_not_bool : nat ≠ bool), which requires @nat_is_not_bool to be of the correct type.

Python translation: https://www.codewars.com/kumite/5b0657957fb2172fe50000a9?sel=5ee8cf1b16e9820028c08c2c