summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2022-12-05 11:28:33 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2022-12-05 11:30:56 +0000
commit1e404cee8e3f36a5fe657012db8ba94c5666cec2 (patch)
tree323956d2fba21ffa668943f3844c807d2af0a0af
parentaa13e2ec1d82ddb20888b1f60230de9798081bae (diff)
Remove import alias.feature/indexed
-rw-r--r--src/Data/Setoid/Indexed/Definition.idr2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Data/Setoid/Indexed/Definition.idr b/src/Data/Setoid/Indexed/Definition.idr
index ab4ac8a..d50af06 100644
--- a/src/Data/Setoid/Indexed/Definition.idr
+++ b/src/Data/Setoid/Indexed/Definition.idr
@@ -3,7 +3,7 @@ module Data.Setoid.Indexed.Definition
import public Control.Relation
-import public Data.Setoid.Definition as Setoid
+import public Data.Setoid.Definition
import Syntax.PreorderReasoning.Setoid