Can someone please explain this? (I'm mostly curious about the last line.)
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.
-- 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).
ℕ ⇔ ℕ^ (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
Something seems to be wrong with the Python tests. This dummy function should pass the first sample test:
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 comment is hidden because it contains spoiler information about the solution
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.”