不能在Idris中使用

Question

我正在尝试使用Idris (0.12.3)中的一些控制代码，特别是DivMod (https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/Nat/DivMod.idr)

但我所做的一切似乎都没有用。我不能用import Data.Nat.DivMod在我的文件中加载它，它返回一个错误Can't find import Data/Nat/DivMod

我试图用标志-p contrib启动idris，但是它没有改变任何东西，idris --listlibs正确地显示了：

base
contrib
effects
prelude
pruviloj

有人知道我如何在代码中加载这个模块吗？

Answer 1

下面的Idris文件是用idris -p contrib编写的

module SO39700630

import Data.Nat.DivMod

x : 10 `DivMod` 4
x = divMod 10 3

使用0.12.3的输出是：

$ stack exec idris -- -p contrib SO39700630
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 0.12.3
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Type checking .\SO39700630.idr
*SO39700630> x
MkDivMod 2 2 (LTESucc (LTESucc (LTESucc LTEZero))) : DivMod 10 4