@@ -45,13 +45,13 @@ A simple test module, with a qualified name of ``Test.NumOps`` can be declared a
46 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
46 assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
47 assertEq g e = if g == e
47 assertEq g e = if g == e
48− then putStrLn "Test Passed"
48+ then putStrLn "."
49− else putStrLn "Test failed"
49+ else putStrLn "F"
51 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
51 assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
52 assertNotEq g e = if not (g == e)
52 assertNotEq g e = if not (g == e)
53− then putStrLn "Test Passed"
53+ then putStrLn "."
54− else putStrLn "Test failed"
54+ else putStrLn "F"
56 testDouble : IO ()
56 testDouble : IO ()
57 testDouble = assertEq (double 2) 4
57 testDouble = assertEq (double 2) 4
@@ -72,4 +72,14 @@ The actual tests are ``testDouble`` and ``testTriple``, and are declared in the
72 , Test.NumOps.testTriple
72 , Test.NumOps.testTriple
75−The testing framework can be invoked using: ``idris --testpkg maths.ipkg``.
75+The testing framework can then be invoked using ``idris --testpkg maths.ipkg``::
77+ > idris --testpkg maths.ipkg
78+ Type checking ./Maths/NumOps.idr
79+ Type checking ./Test/NumOps.idr
80+ Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
84+Note how both tests have reported success by printing a single ``.``
85+as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.