Merge pull request #23 from stefan-hoeck/export_infix

[ compat ] adjust to upstream changes
stefan-hoeck · Apr 5, 2024 · 0620a33 · 0620a33
2 parents 5235473 + 8bc38d1
commit 0620a33
Show file tree

Hide file tree

Showing 13 changed files with 26 additions and 0 deletions.
diff --git a/docs/src/Intro.md b/docs/src/Intro.md
@@ -6,6 +6,8 @@ assumed to hold for all values of the refinement type.
 ```idris
 module Intro
 
+import Control.Relation.ReflexiveClosure
+import Control.Relation
 import Language.Reflection.Pretty
 import Language.Reflection.Util
 import Derive.Prelude

diff --git a/json/test/src/Main.idr b/json/test/src/Main.idr
@@ -1,5 +1,7 @@
 module Main
 
+import Control.Relation
+import Control.Relation.ReflexiveClosure
 import Data.Refined.Bits32
 import Data.Refined.Int8
 import Data.Refined.String

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.ReflexiveClosure
+import Control.Relation
 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.ReflexiveClosure
+import Control.Relation
 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.ReflexiveClosure
+import Control.Relation
 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.ReflexiveClosure
+import Control.Relation
 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.ReflexiveClosure
+import Control.Relation
 import public Data.Prim.Char
 import public Data.Refined.Core
 

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.ReflexiveClosure
+import Control.Relation
 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.ReflexiveClosure
+import Control.Relation
 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.ReflexiveClosure
+import Control.Relation
 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.ReflexiveClosure
+import Control.Relation
 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.ReflexiveClosure
+import Control.Relation
 import public Data.Prim.Integer
 import public Data.Refined.Core
 

diff --git a/tsv/test/src/Main.idr b/tsv/test/src/Main.idr
@@ -1,5 +1,7 @@
 module Main
 
+import Control.Relation.ReflexiveClosure
+import Control.Relation
 import Data.Refined.Bits32
 import Data.Refined.Int8
 import Data.Refined.String