The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

kmeredith (23) [Avatar] Offline
Ch 9's definition of `Finished` consist of:

data Finished : Type where
  Lost : (game : WordState 0 (S letters))  -> Finished
  Won  : (game : WordState (S guesses) 0 ) -> Finished

It seems to me that a `Won` case would involve both 0 words and guesses left.

Perhaps this case doesn't apply to the implementation of Hangman in this excellent text?
kmeredith (23) [Avatar] Offline
Actually, looking at the type of `processGuess`, guessing correctly does not appear to cost a guess!

processGuess : (letter : Char) ->
               WordState (S guesses) (S letters) ->
               Either (WordState guesses    (S letters))
                      (WordState (S guesses) letters)