Convert proof into Game level: metric - lvl 3 - Githubissues

lnay / metric-spaces-and-topology-game

MIT License

2 stars 1 forks source link

Convert proof into Game level: metric - lvl 3 #15

Open lnay opened 5 months ago

lnay commented 5 months ago

Make sure issue #7 is resolved
Take the corresponding file in Game/Levels/content_drafts and repurpose into a level file in Game/Levels/<world>/
Make sure to import the new file in the corresponding world lean file Game/Levels/<world>.lean
Add a new issue to gather feedback on the new level

Have a look at game creation instructions and existing levels for some guidance, and submit pull request for more from a maintainer.

Things that this task should take into consideration:

Add suitable markdown introducing the level
Add suitable hints and branches
unlock necessary theorems and definitions for the level

Syllabus outline is here #5 as a reference, potentially useful for context to the level.

lnay commented 4 months ago

I'm taking this one