From a9230817da88305b16d658a056e72bef159b8f94 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 11 Sep 2024 13:59:17 +0100 Subject: Define terms. --- src/Inky/Type.idr | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/Inky/Type.idr') 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 -- cgit v1.2.3