%inline

lib/Quox/Syntax/Shift.idr

@@ -110,7 +110,7 @@ export
 ssDownEqv SZ      = EqSS EqSZ
 ssDownEqv (SS by) = EqSS $ ssDownEqv by
 
-private
+private %inline
 ssDownViaNat : Shift (S from) to -> Shift from to
 ssDownViaNat by =
   rewrite shiftDiff by in
@@ -125,12 +125,12 @@ shift : Shift from to -> Var from -> Var to
 shift SZ      i = i
 shift (SS by) i = VS $ shift by i
 
-private
+private %inline
 shiftViaNat' : (by : Shift from to) -> (i : Var from) ->
                (0 p : by.nat + i.nat `LT` to) -> Var to
 shiftViaNat' by i p = V $ by.nat + i.nat
 
-private
+private %inline
 shiftViaNat : Shift from to -> Var from -> Var to
 shiftViaNat by i = shiftViaNat' by i $ shiftVarLT by i
 
@@ -163,12 +163,12 @@ compNatProof by bz =
   0 (>>>) : a = b -> b = c -> a = c
   x >>> y = trans x y
 
-private
+private %inline
 compViaNat' : (by : Shift from mid) -> (bz : Shift mid to) ->
               Shift from (by.nat + bz.nat + from)
 compViaNat' by bz = fromNat $ by.nat + bz.nat
 
-private
+private %inline
 compViaNat : (by : Shift from mid) -> (bz : Shift mid to) -> Shift from to
 compViaNat by bz = rewrite compNatProof by bz in compViaNat' by bz
 
@@ -207,12 +207,13 @@ public export
 interface CanShift f where
   (//) : f from -> Shift from to -> f to
 
-export CanShift Var where i // by = shift by i
+export %inline
+CanShift Var where i // by = shift by i
 
 namespace CanShift
-  public export
+  public export %inline
   [Map] (Functor f, CanShift tm) => CanShift (f . tm) where
     x // by = map (// by) x
 
-  public export
+  public export %inline
   [Const] CanShift (\_ => a) where x // _ = x