leanprover-community
There is no responsive answer from the game after executing command
Hi everyone, currently I am learning lean, I have executed the command but it doesn't give me the respond in the lesson 3/9:cake from swap from the tutorial party snack of Intro to logic. I have reloaded multiple times but it still haven't solved the problem yet.
Its definitely a bug hat this doesn't display a fatal error to the user.
You need to always use a tactic, so you need to start with exact or apply or anything else you find under "Tactics". (this is because this is a tactic-proof, similar to what you het in Lean with writing := by at the beginning of your proof.
The hint (in yellow) of that gane isn't super obvious, it means to show you which "term" you feed to one of the two "tactics" above
(concretely here you "Retry" your last command and write exact before what's written)
Suggestions to change the hint would go to the github repo of the logic game. Unfortunately Im on mobile so don't have the link rn.
In any case, thanks for reaching out! I'll mark this as "bug" to investigate the missing response from the server.