Made fromIntegerNat use case instead of if

[SaraWolffs]

Using if with an assert_smaller could cause infinite compile-time looping. To prevent this, a pattern match on 0 was needed, but functions that match on Integers don't reduce in proofs. This should fix that for fromIntegerNat by avoiding the original issue (tested, this version doesn't loop on \i=>fromIntegerNat i at the REPL, which the old version did without the 0 match).

The new code has been tested correct for (-1), 0, 5, 10, 100, 1000 and 1234. It does seem to be slightly slower than the original, but neither is very fast. Proving things for Integer is probably still not a good idea, but it should now at least be possible to convert a So (i > 0) to an IsSucc (fromIntegerNat i), in theory (untested, I'm bad at proofs, but compute does now reduce fromIntegerNat i to a case block).

As a minor simultaneous change, the fromIntegerNat takes an argument i, for Integer, rather than n for Nat.

[SaraWolffs]

The appveyor build is failing (travis build as well), but I can't for the life of me see why. Relevant bits of the log:

Type checking .\Prelude\Nat.idr
.
.
.
Type checking .\Data\Bits.idr
Uncaught error: user error (Pattern match failure in do expression at src\Idris\Elab\Transform.hs:32:10-72)

The compiler itself builds just fine. Prelude.Nat still typechecks fine. So do lots of other libraries, and Data.Bits was left untouched, as was all Haskell code. Locally, building with Stack works fine. But when typechecking Data.Bits, the test environment fails a Haskell pattern match.

Looking at Transform.hs, it seems to expect an ElabResult with an empty (that is, []) resultCaseDecls field, which is the only part of the pattern match that looks like it could fail. Since I did add a case block, this seems at least related, but I'm still not sure how this case caused a problem but nothing else did.

[melted]

Thanks for the PR!

I'll try and see what happens.