不能在 Idris 中使用 contrib

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 它 returns 一个错误 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

不能在 Idris 中使用 contrib

Can't use the contrib in Idris

idris