Loading collection data...
Collections are a way for you to organize kata so that you can create your own training routines. Every collection you create is public and automatically sharable with other warriors. After you have added a few kata to a collection you and others can train on the kata contained within the collection.
Get started now by creating a new collection.
I can reproduce. This is hard to debug without having access to the exact contents of Preloaded.lean [do I have access to this file?]
This comment is hidden because it contains spoiler information about the solution
I made a solution in VS Code (Lean 3.7.2) but it doesn't work on this site. Could there be some subtle difference between the contents of the Preloaded import and the definitions commented out in the answer template?