From 27e61011acafde98d52993c6c6a2fb917f670263 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 19 Feb 2023 17:43:14 +0100
Subject: [PATCH] %inline

---
 lib/Quox/Equal.idr        | 2 +-
 lib/Quox/Syntax/DimEq.idr | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index c349dfc..ba5fd48 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -188,7 +188,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
 
     ||| compares two types, using the current variance `mode` for universes.
     ||| fails if they are not types, even if they would happen to be equal.
-    export covering
+    export covering %inline
     compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
     compareType ctx s t = do
       let Element s ns = whnfD defs s
diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index 6d9e444..d761bcb 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -28,11 +28,11 @@ data DimEq : Nat -> Type where
 %name DimEq eqs
 
 
-export
+export %inline
 zeroEq : DimEq 0
 zeroEq = C [<]
 
-export
+export %inline
 new' : {d : Nat} -> DimEq' d
 new' {d = 0}   = [<]
 new' {d = S d} = new' :< Nothing