From b0499ebed669864d1ad13837066ce4a0c31078a0 Mon Sep 17 00:00:00 2001 From: stefan-hoeck Date: Sun, 21 Jan 2024 09:29:25 +0000 Subject: [PATCH] [ refactor ] fewer public exports --- pack.toml | 2 +- src/Data/Refined/Bits16.idr | 2 ++ src/Data/Refined/Bits32.idr | 2 ++ src/Data/Refined/Bits64.idr | 2 ++ src/Data/Refined/Bits8.idr | 2 ++ src/Data/Refined/Char.idr | 2 ++ src/Data/Refined/Core.idr | 2 +- src/Data/Refined/Int16.idr | 2 ++ src/Data/Refined/Int32.idr | 2 ++ src/Data/Refined/Int64.idr | 2 ++ src/Data/Refined/Int8.idr | 2 ++ src/Data/Refined/Integer.idr | 2 ++ src/Data/Refined/String.idr | 2 +- 13 files changed, 23 insertions(+), 3 deletions(-) diff --git a/pack.toml b/pack.toml index e885aec..342a088 100644 --- 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 index 6cf5e85..3feb16e 100644 --- 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 index 0414124..c710853 100644 --- 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 index 9f4fcff..26a5359 100644 --- 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 index 32036dd..8ea71d5 100644 --- 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 index 65e583f..a63f9dc 100644 --- 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 index 408a816..8ef3d4b 100644 --- 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 index 956e713..4701bf5 100644 --- 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 index 2e2e404..765043f 100644 --- 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 index fbd83a0..d3ef0cb 100644 --- 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 index 57059ba..ad4f067 100644 --- 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 index 3f395bc..6414c3c 100644 --- 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 index 74966d2..17669e4 100644 --- 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