Can't use the contrib in Idris [closed]

Question

I'm trying to use some of the contrib code in Idris (0.12.3), specifically DivMod (https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/Nat/DivMod.idr)

But nothing that I do seems to work. I can't load it in my file with import Data.Nat.DivMod it returns an error Can't find import Data/Nat/DivMod

I tried to start idris with the flag -p contrib but it doesn't change anything and idris --listlibs shows correctly :

base
contrib
effects
prelude
pruviloj

Does anyone know how I can load this module in my code ?

Answer 1

The following Idris file typechecks with idris -p contrib:

module SO39700630

import Data.Nat.DivMod

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

The output using 0.12.3 is:

$ 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