A 'game'/interactive tutorial for items other than proofs

Stream: Lean for teaching

[Tristan Figueroa-Reid]

Were there ever plans to (in where either lean4game would be extended or new resources would be made) design interactive exercises for learning lean4 past the tactic mode? The logic and natural number games are good for teaching tactics and the general flow of lean4 proofs, but I haven't seen any good exercise for any other part of lean in the wild.

[Patrick Massot]

Did you read #fpil? They are exercises there.

[Kevin Buzzard]

#tpil makes you do all the exercises in the first four sections in term mode without even letting you know that tactics even exist! It's very much designed to teach you the concept of types and terms and how they relate to theorems and proofs in a functional language.

[Luigi Massacci]

(deleted)