%inline, etc

tests/TAP.idr

@@ -8,7 +8,8 @@ import Control.Monad.Reader
 import Control.Monad.State
 import System
 
-public export Info : Type
+public export
+Info : Type
 Info = List (String, String)
 
 private
@@ -42,7 +43,7 @@ All ToInfo es => ToInfo (OneOf es) where
   toInfo (One Here      value) = toInfo value
   toInfo (One (There x) value) = toInfo (One x value)
 
-export ToInfo () where toInfo () = []
+export %inline ToInfo () where toInfo () = []
 
 export
 data Test = One TestBase | Group String (List Test)
@@ -83,7 +84,7 @@ export %inline
 
 
 
-export
+export %inline
 header : List a -> String
 header tests = "1..\{show $ length tests}"
 
@@ -92,15 +93,15 @@ private
 Runner : Type -> Type
 Runner = ReaderT Nat IO
 
-private
+private %inline
 putIndentLines : List String -> Runner ()
 putIndentLines xs = traverse_ (putStrLn . indent !ask) xs
 
-private
+private %inline
 isOk : Bool -> String
 isOk b = if b then "ok" else "not ok"
 
-private
+private %inline
 toBool : Result -> Bool
 toBool (Tried ok _) = ok
 toBool _ = True