Can someone please explain this? (I'm mostly curious about the last line.)

Fixed

Before I could start coding, I had to manually concatenate the preloaded snippets interspersed through the description and hunt down some missing imports. Please make the preloaded part directly copy+pasteable and/or uncommentable.

Thanks for the info. Changed the description and tests.

From Preloaded:

-- Cartesian powers of ℕ. Zeroth power is nonsense.
ℕ×ℕ^ : ℕ → Set
ℕ×ℕ^ zero = ℕ
ℕ×ℕ^ (suc n) = ℕ × ℕ×ℕ^ n

The zeroth power is not nonsense; it serves as a base case in the natural definition

ℕ^ : ℕ → Set
ℕ^ zero = ⊤
ℕ^ (suc n) = ℕ × ℕ^ n

and falls out automatically from the other natural definition

ℕ^ : ℕ → Set
ℕ^ n = Fin n → ℕ

Of course, task 2 would then need to change to ℕ ⇔ ℕ^ (suc n).

That was clearly wrong, so I fixed the test to expect a set with an empty array.

Oops, this version has a bug with a small number of (untested) inputs, see the fixed version.

Thanks for issuing
Seemed that i did too much on anti-cheat
Fixed

Thanks! Edited.

Something seems to be wrong with the Python tests. This dummy function should pass the first sample test:

def kcuf(code):
    return ',>' + 66 * '+' + '.' + 55 * '+' + '.' + 20 * '-' + '.<.'

but it crashes with

Traceback (most recent call last):
  File "main.py", line 21, in <module>
  File "main.py", line 9, in Check
  File "/home/codewarrior/setup.py", line 137, in <lambda>
  File "/home/codewarrior/setup.py", line 107, in __BF__
NameError: name 'len' is not defined

(I tried both Python 3.4.3 and Python 3.6.0 with the same result.)

Yeah, I was a bit too daft to think of a suitable type class =/
So I just left that challenge alone.

Thank you! I have submitted a new solution where invalid programs do not typecheck.

This doesn’t satisfy “An invalid program should raise a type error rather than a runtime error.”

This doesn’t satisfy “An invalid program should raise a type error rather than a runtime error.”