hangman.idr:204:8-12: | 204 | wlen = proof search | ~~~~~ This style of tactic proof is deprecated. See %runElab for the replacement. ---- 6 guesses left Enter guess: Good guess! -a-a 6 guesses left Enter guess: No, sorry -a-a 5 guesses left Enter guess: No, sorry -a-a 4 guesses left Enter guess: No, sorry -a-a 3 guesses left Enter guess: Good guess! ja-a 3 guesses left Enter guess: Good guess! You won! Successfully guessed java