Невозможно использовать вно в Идриса

Question

Я пытаюсь использовать часть кода вно в Идриса (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 --listlibs правильно показывает:

base 
contrib 
effects 
prelude 
pruviloj 

Кто-нибудь знает, как я могу загрузить этот модуль в свой код?

Answer 1

Следующие файл typechecks Идрис с 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