git.iko.soy/Idris-dev
on master help sign in
Make `divides` views public
cb7c850Alex Gryzlov
libs/base/Data/Primitives/Views.idr+2−2
compare with master
unifiedsplit
@@ -14,7 +14,7 @@ namespace Integer
14 Divides ((d * div) + rem) d
14 Divides ((d * div) + rem) d
15
15
16 ||| Covering function for the `Divides` view
16 ||| Covering function for the `Divides` view
17− export
17+ public export
18 divides : (val : Integer) -> (d : Integer) -> Divides val d
18 divides : (val : Integer) -> (d : Integer) -> Divides val d
19 divides val 0 = DivByZero
19 divides val 0 = DivByZero
20 divides val d
20 divides val d
@@ -51,7 +51,7 @@ namespace Int
51 -- TODO: Someone please check this and fix if necessary...
51 -- TODO: Someone please check this and fix if necessary...
52
52
53 ||| Covering function for the `Divides` view
53 ||| Covering function for the `Divides` view
54− export
54+ public export
55 divides : (val : Int) -> (d : Int) -> Divides val d
55 divides : (val : Int) -> (d : Int) -> Divides val d
56 divides val 0 = DivByZero
56 divides val 0 = DivByZero
57 divides val d
57 divides val d