Bug: in natural number game, "The tactic 'induction' is not available in this game!" where it should be available

leanprover-community / lean4game

Server to host lean games.

https://adam.math.hhu.de

GNU General Public License v3.0

197 stars 35 forks source link

Closed noamraph closed 9 months ago

noamraph commented 9 months ago

In https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Addition/level/1, I type induction n with d hd, and I get "The tactic 'induction' is not available in this game!", although the instructions say to use it.

joneugster commented 9 months ago

Been fixed today :+1: