cannot apply succ_inj in succ_mul

Open bombless opened this issue 7 months ago • 3 comments

its in the panel on the right, so my guess is it's a bug that the execution report error as "unknown identifier 'succ_inj'"

May 20 '25 03:05 bombless

The panel could probably be improved (I think at the moment it actually lists everything that you have already unlocked?), but then you don't need that for this level anyway.

May 31 '25 03:05 user202729

that's true, but that can also be a feature. just that you don't want to confuse the user

Jun 04 '25 06:06 bombless

Same as https://github.com/leanprover-community/lean4game/issues/187

Sep 23 '25 21:09 joneugster