[ export ] public export the most common modules from algebra

stefan-hoeck · Apr 5, 2024 · 9bf2671 · 9bf2671
1 parent 0620a33
commit 9bf2671
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Data/Refined.idr b/src/Data/Refined.idr
@@ -1,5 +1,7 @@
 module Data.Refined
 
+import public Control.Relation
+import public Control.Relation.ReflexiveClosure
 import public Data.List
 import public Data.Refined.List
 import public Data.Refined.Nat