@@ -108,16 +108,15 @@ effect signature:
108108 Guess : (x : Char) ->
109109 sig MysteryRules Bool
110110 (Mystery (Running (S g) (S w)))
111− (\inword =>
112− Mystery (case inword of
113− True => (Running (S g) w)
114− False => (Running g (S w))))
111+ (\inword => if inword
112+ then Mystery (Running (S g) w)
113+ else Mystery (Running g (S w)))
115114 Won : sig MysteryRules () (Mystery (Running g 0))
116115 (Mystery NotRunning)
117116 Lost : sig MysteryRules () (Mystery (Running 0 g))
118117 (Mystery NotRunning)
119118 NewWord : (w : String) ->
120− sig MysteryRules () h (Mystery (Running 6 (length (letters w))))
119+ sig MysteryRules () (Mystery NotRunning) (Mystery (Running 6 (length (letters w))))
121120 Get : sig MysteryRules String (Mystery h)
122121
123122This description says nothing about how the rules are implemented. In
@@ -243,11 +242,11 @@ running ``game``:
243242.. code-block:: idris
244243
245244 runGame : Eff () [MYSTERY NotRunning, RND, SYSTEM, STDIO]
246− runGame = do srand (cast !time)
247− let w = index !(rndFin WEWEWE) words
248− NewWord w
245+ runGame = do srand !time
246+ let w = index !(rndFin _) words
247+ call $ NewWord w
249248 game
250− putStrLn !Get
249+ putStrLn !(call Get)
251250
252251We use the system time (``time`` from the ``SYSTEM`` effect; see
253252Appendix :ref:`sect-appendix`) to initialise the random number