From 6e8ab4c1135f39d441cdcf54c5a1bc12b7e565be Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 8 Apr 2023 15:45:24 +0100
Subject: Prove conversion is a generic equality.

---
 src/Core/Declarative.idr | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/Core/Declarative.idr')

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 8704e07..e5aa95a 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -287,6 +287,7 @@ wknPresTermWf :
   EnvWf env2 ->
   IsExtension thin env2 env1 ->
   TermWf env2 (wkn t thin) (wkn a thin)
+export
 wknPresTermConv :
   {0 env1 : Env sx} ->
   TermConv env1 t u a ->
-- 
cgit v1.2.3