TentativeConvert

This is related to https://github.com/leanprover-community/lean4game/issues/299. The plan is that in future versions of lean4game, enabling `exact` will no longer automatically enable `exact?`, see https://github.com/leanprover-community/lean4game/pull/304#issuecomment-2708478515. That should solve this issue.

What would the fix proposed here actually do? I’d say the ideal behaviour would be that `simp?` and `apply?` are treated like any other tactic, i.e. that it is left...

Thanks for clarifying! (I’ll leave it to @joneugster to merge when dev is ready.)

I would argue that the info message spoils the point of disallowing `apply?`. So it would be better to ensure that disallowed tactics don't generate any messages.

I was tought that starting a sentence with a non-natural-language word is bad style. But the above difference in rendering is clearly a bug rather than a feature. In Robo,...

I'm not sure this is fixed. Running Robo with lean4game tag v4.22.0 locally, I can still use `apply?` (even with rules set to strict). I don't think the `apply?` tactic...

Is “three major tabs Tactic/Theorems/Defs” planned or already implemented in some version? I had a vague memory of that plan, and wrote the issue because I think this alternative might...

@dlebedinsky To see the solutions, you need to look in the repository of the game you're playing, e.g. https://github.com/leanprover-community/NNG4 for the Natural Number Game. You’ll find all solutions under `Game/Levels`....