summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder/Term.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
-rw-r--r--src/Soat/FirstOrder/Term.idr5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 2712c88..07ab248 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -1,14 +1,13 @@
module Soat.FirstOrder.Term
-import Control.Relation
+import Data.Morphism.Indexed
+import Data.Setoid.Indexed
import Soat.Data.Product
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Signature
-import Soat.Relation
%default total
-%hide Control.Relation.Equivalence
public export
data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where