@@ -108,16 +108,15 @@ effect signature:
108 Guess : (x : Char) ->
108 Guess : (x : Char) ->
109 sig MysteryRules Bool
109 sig MysteryRules Bool
110 (Mystery (Running (S g) (S w)))
110 (Mystery (Running (S g) (S w)))
111− (\inword =>
111+ (\inword => if inword
112− Mystery (case inword of
113− True => (Running (S g) w)
112+ then Mystery (Running (S g) w)
114− False => (Running g (S w))))
113+ else Mystery (Running g (S w)))
115 Won : sig MysteryRules () (Mystery (Running g 0))
114 Won : sig MysteryRules () (Mystery (Running g 0))
116 (Mystery NotRunning)
115 (Mystery NotRunning)
117 Lost : sig MysteryRules () (Mystery (Running 0 g))
116 Lost : sig MysteryRules () (Mystery (Running 0 g))
118 (Mystery NotRunning)
117 (Mystery NotRunning)
119 NewWord : (w : String) ->
118 NewWord : (w : String) ->
120− sig MysteryRules () h (Mystery (Running 6 (length (letters w))))
119+ sig MysteryRules () (Mystery NotRunning) (Mystery (Running 6 (length (letters w))))
121 Get : sig MysteryRules String (Mystery h)
120 Get : sig MysteryRules String (Mystery h)
123This description says nothing about how the rules are implemented. In
122This description says nothing about how the rules are implemented. In
@@ -243,11 +242,11 @@ running ``game``:
243.. code-block:: idris
242.. code-block:: idris
245 runGame : Eff () [MYSTERY NotRunning, RND, SYSTEM, STDIO]
244 runGame : Eff () [MYSTERY NotRunning, RND, SYSTEM, STDIO]
246− runGame = do srand (cast !time)
245+ runGame = do srand !time
247− let w = index !(rndFin WEWEWE) words
246+ let w = index !(rndFin _) words
248− NewWord w
247+ call $ NewWord w
250− putStrLn !Get
249+ putStrLn !(call Get)
252We use the system time (``time`` from the ``SYSTEM`` effect; see
251We use the system time (``time`` from the ``SYSTEM`` effect; see
253Appendix :ref:`sect-appendix`) to initialise the random number
252Appendix :ref:`sect-appendix`) to initialise the random number