Search code examples
doublenatidrisfloor

Idris, convert from a Double to a Nat by dropping the decimal points (floor)

In Idris, how to convert from a Double to a Nat by floor, dropping the decimal points. I tried cast:

cast {to=Nat} num

However did not work.

When checking an application of function Main.takeLeftOfHalfLength:
        Can't cast from Double to Nat

Well that's to be expected as its not very explicit how the cast would work, loss of information.

However I still wish to cast from Double to Nat, how can it be done?

I discovered divNat function which lets me divide a Nat, but I'll leave the question here

Solution

  • We can use floor, cast to Integer and then use integerToNat:

    Main> integerToNat $ cast {to = Integer} $ floor 3.9
3

    Similarly ceiling can be used to get the rounded up Nat:

    Main> integerToNat $ cast {to = Integer} $ ceiling 3.9
4