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

user_78000 0
Viewed 57

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

idris nat floor double
1 Answers

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
user_3676490
Related