add all-your-base exercise

[oxe-i]

I had many doubts about the difficulty of this one.

This exercise is usually low medium in difficulty (4 or 5), but I made a point of setting arguments to dependent types that enforce restrictions, instead of checking for errors. This is usually more idiomatic and a strong point of Lean, because any invalid argument generates a compiler error and specifications are fully described by the type system.

The problem is that, in order to use those types, arguments must carry with themselves the proof of their validity. But proving things is very different from usual programming practice and more close to mathematics, so the difficulty should be raised to reflect this. But how much?

What do you think?

[keiravillekode]

Yes, using List (Fin outputBase.val) makes all-your-base harder on this track, so it reasonable to increase the difficulty. If we end up with 5 or more Hard exercises so students can earn Difficult trophies, that will be excellent.

Exercism once had binary trinary octal and hexadecimal exercises, each with error-detecting test cases where the input contained invalid characters. These were deprecated for all-your-base. Because we avoid bad-digit test cases in Lean all-your-base, perhaps we should implement one of the old exercises, perhaps hexadecimal