search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
137 stars 25 forks source link

bug: stuck on unexpected end of input #222

Closed bjarki781 closed 2 months ago

bjarki781 commented 2 months ago

I've been enjoying the game so far but I'm currently stuck on an error, which looks like a bug. In level 3/11 of implication world I copy and paste the tactics that are given on the side and I get the error No Goals - unexpected end of input and am unable to continue.

Screenshot 2024-04-28 at 11 38 26 Screenshot 2024-04-28 at 11 38 40
joneugster commented 2 months ago

that seems to work as expected. exacttakes an argument, for example exact h1.

Maybe you could read the text (hints & inventory entry on exact) and comment if you have suggestions how the wording of these could be improved!

bjarki781 commented 2 months ago

Ah, this is a bit awkward :) Had been enough to go back to the last level. But since we had been using rfl as a kind of QED until that point and tactics that guess the input, it would be helpful to say explicitly in level 1 "The exact tactic can be used to close a goal which is exactly one of the hypotheses. It takes that hypothesis as an argument." or something of that sort.

joneugster commented 2 months ago

All good! Learning games are here to learn and make mistakes :)

I added a sentence to NNG like you suggested