From 0ecd9e608ced18f70f465c986d6519e8e95b0b6b Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 20 Nov 2024 15:31:25 +0000
Subject: Improve syntactic sugar.

Sugar makes programs nicer to write.
---
 src/Inky/Term/Checks.idr | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/Inky/Term/Checks.idr')

diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 402f623..829561a 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -204,6 +204,7 @@ fallbackCheck prf p a =
     (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $
   (b := p) >=> alpha b a
 
+export
 synths :
   (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
   (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
-- 
cgit v1.2.3