summaryrefslogtreecommitdiff
path: root/src/Data/Setoid/Indexed.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Setoid/Indexed.idr')
-rw-r--r--src/Data/Setoid/Indexed.idr4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Data/Setoid/Indexed.idr b/src/Data/Setoid/Indexed.idr
new file mode 100644
index 0000000..5e9ef46
--- /dev/null
+++ b/src/Data/Setoid/Indexed.idr
@@ -0,0 +1,4 @@
+||| An indexed setoid is a type family equipped with a homogeneous equivalence relation
+module Data.Setoid.Indexed
+
+import public Data.Setoid.Indexed.Definition