TicTacToe in Lean Manual

Stream: general

[Burkhardt Renz]

In https://sebasti.a.nullri.ch/lean4/doc/monads/states.lean.html there is an implementation of tic-tac-toe as an example for the state monad.
In version leanprover/lean4:v4.26.0-rc2 I got two errors in that file:

1. in function playGamethe line while true do
2. in function tic-tac-toethe let gs := { .... }

Can anybody help to fix that?

[Aaron Liu]

What are the errors? Can you post the code you used? I'm looking at the page right now and see a lot more errors.

[Kevin Buzzard]

I don't know anything about monads but that looks like a pretty suspicious link you're giving. Are you sure that's the official "Lean Manual"? (It might be, but I was expecting something hosted by the lean FRO)

[Aaron Liu]

some of the content seems to be from this file https://github.com/leanprover/lean4/tree/master/doc/examples

[Chris Henson]

That link is under Sebastian's domain. It's the old mdbook manual that was removed about a year ago, previously under lean4/doc.

[Chris Henson]

The PR that removed this was lean4#6401. If I take the file doc/monads/states.lean that is removed there and update the hashmap import to Batteries.Data.HashMap, everything seems to work as expected. If you post an #mwe someone may diagnose what you are running into.

[Burkhardt Renz]

Hi Chris,
you are right.

But as soon as I import Mathlib instead of Batteries.Data.HashMap I get the error in line 157 and in line 164.

[Burkhardt Renz]

I managed to fix the problems. When replacing Batteries.HashMap with Std.HashMap, we need to change one function (empty => emptyWithCapacity) and some types.
Here the fixed file: https://esb-dev.github.io/mat/FPLTicTacToe.lean