summaryrefslogtreecommitdiff
path: root/src/Inky/Type.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky/Type.idr')
-rw-r--r--src/Inky/Type.idr8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index aadd968..3021f96 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -38,6 +38,14 @@ export
Injective TVar where
injective Refl = Refl
+export
+Injective TUnion where
+ injective Refl = Refl
+
+export
+Injective TProd where
+ injective Refl = Refl
+
-- Equality --------------------------------------------------------------------
export