From 9bf2671914d011b844a96277f28d63abe57564ce Mon Sep 17 00:00:00 2001 From: stefan-hoeck Date: Fri, 5 Apr 2024 04:52:20 +0000 Subject: [PATCH] [ export ] public export the most common modules from algebra --- src/Data/Refined.idr | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Data/Refined.idr b/src/Data/Refined.idr index 2906eb7..51b1ffe 100644 --- 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