A theorem/tactic that will be unlocked at some point in the game might throw "unknown identifier" if it is not imported in a previous level in the lean file. Instead, we should modify the error message to say "not available yet" or something more reasonable.
A theorem/tactic that will be unlocked at some point in the game might throw "unknown identifier" if it is not imported in a previous level in the lean file. Instead, we should modify the error message to say "not available yet" or something more reasonable.
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Natural.20Number.20Game/near/417407951