I agree that Lean or any of the other languages I listed would be a better choice then Idris and despite how I wrote my original post I wouldn't recommend Idris to someone who explicitly wanted a theorem prover.