Idris，通过去掉小数点将 Double 转换为 Nat（下限）

Question

在 Idris 中，如何按楼层从 Double 转换为 Nat，去掉小数点。 我试过演员：

cast {to=Nat} num

但是没有用。

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

这是意料之中的，因为它不是很明确演员将如何工作，信息丢失。

但是我还是想从 Double 转换为 Nat，怎么做？

---

我发现了 divNat 函数，它可以让我划分一个 Nat，但我将把问题留在这里

Answer 1

我们可以使用floor，转换为Integer，然后使用integerToNat：

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

类似地，ceiling 可用于取整 Nat：

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