Skip to content

Strong induction / lt world first draft#93

Open
kvanvels wants to merge 36 commits into
leanprover-community:mainfrom
kvanvels:kvv_lt
Open

Strong induction / lt world first draft#93
kvanvels wants to merge 36 commits into
leanprover-community:mainfrom
kvanvels:kvv_lt

Conversation

@kvanvels

Copy link
Copy Markdown

First draft of strong induction world.

@joneugster

Copy link
Copy Markdown
Collaborator

Is this ready for review? If so, it would be @kbuzzard 's review that would be needed.

(Otherwise, could you mark the PR as "draft" until it is ready)

@joneugster joneugster added the new content Issues/PRs adding new game content label Sep 27, 2025
@kvanvels

Copy link
Copy Markdown
Author

Hi, I think the ball is in @kbuzzard 's court. I think it is ready for a review but he doesn't have the time to review it. I think this will probably die on the vine.

@joneugster

Copy link
Copy Markdown
Collaborator

Hi, I'm afraid this might not be moving anywhere. As I feel the authority over this game's content is in Kevin Buzzards hands, I don't feel like I should accept these PRs myself.

I would suggest the following: Create a new game "NNG-community" or something (a new github project) which contains the new worlds from this PR and the next one.

Then give me a text on Zulip so I can:

  • move your new repo to `leanprover-community/NNG-community (optional; if desired)
  • ensure the game gets displayed on the game server

This way yous could have the review authority to add more content and people could play it and we don't need to depend on reviews here!

Would that sound reasonable? Sorry for how slow things move...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

new content Issues/PRs adding new game content

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants