The random tests incorrectly expect it to be possible to delete a class attribute from an instance. On a normal Python class, this raises an AttributeError. Solutions that preserve this normal behavior should be accepted.

Am I the only one who followed the directions and wrote an infinite stream (up to integer precision) rather than sieving to a predefined limit?

Agda test cases should not open the solution; that can often be exploited to bring unexpected definitions into scope.

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.

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.

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.)

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.”

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.”

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.”