kmeredith (23) [Avatar] Offline
#1
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
#2
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)