[ refactor ] fewer public exports

stefan-hoeck · Jan 21, 2024 · b0499eb · b0499eb
1 parent db4fc19
commit b0499eb
Show file tree

Hide file tree

Showing 13 changed files with 23 additions and 3 deletions.
diff --git a/pack.toml b/pack.toml
@@ -33,7 +33,7 @@ ipkg = "test.ipkg"
 [custom.all.algebra]
 type   = "git"
 url    = "https://github.com/stefan-hoeck/idris2-algebra"
-commit = "latest:main"
+commit = "latest:export"
 ipkg   = "algebra.ipkg"
 
 [custom.all.json-simple]

diff --git a/src/Data/Refined/Bits16.idr b/src/Data/Refined/Bits16.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Bits16
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Bits16
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Bits32.idr b/src/Data/Refined/Bits32.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Bits32
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Bits32
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Bits64.idr b/src/Data/Refined/Bits64.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Bits64
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Bits64
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Bits8.idr b/src/Data/Refined/Bits8.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Bits8
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Bits8
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Char.idr b/src/Data/Refined/Char.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Char
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Char
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Core.idr b/src/Data/Refined/Core.idr
@@ -1,6 +1,6 @@
 module Data.Refined.Core
 
-import public Data.DPair
+import Data.DPair
 import public Data.Maybe0
 import public Decidable.HDec
 

diff --git a/src/Data/Refined/Int16.idr b/src/Data/Refined/Int16.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Int16
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Int16
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Int32.idr b/src/Data/Refined/Int32.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Int32
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Int32
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Int64.idr b/src/Data/Refined/Int64.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Int64
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Int64
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Int8.idr b/src/Data/Refined/Int8.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Int8
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Int8
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/Integer.idr b/src/Data/Refined/Integer.idr
@@ -1,5 +1,7 @@
 module Data.Refined.Integer
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import public Data.Prim.Integer
 import public Data.Refined.Core
 

diff --git a/src/Data/Refined/String.idr b/src/Data/Refined/String.idr
@@ -1,6 +1,6 @@
 module Data.Refined.String
 
-import public Data.Refined.Char
+import Data.Refined.Char
 import public Data.Refined.List
 import public Data.Refined.Core