A backtracking quasigroup completion solver whose solutions are verified correct, written in Idris.