Giter Club home page Giter Club logo

stg4's Introduction

STG4

This is the Set Theory Game. It uses the Lean4 Game Engine and it is hosted at adam.math.hhu.de.

Getting Started

There are multiple ways to run the game while developing it:

VSCode Devcontainer

The full instructions are at Running games locally. In particular, the recommended setup is to have docker installed on your computer and then click on the pop-up "Reopen in Container" which is shown when opening this project in VSCode.

You can then open localhost:3000 in a browser.

After making changes to the code, you need to run lake build in a terminal and reload the web page inside the "Simple Browser".

Codespaces

You can work on it using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for for example under "Ports" and clicking on "Open in Browser".

Note: You have to wait until npm started properly. In particular, this is after a message like [client] webpack 5.81.0 compiled successfully in 38119 ms appears in the terminal, which might take a good while.

As with devcontainers, you need to run lake build after changing any lean files and then reload the browser.

Local setup

The full instructions are at Running games locally. In particular, the recommended setup is to have docker installed on your computer and then click on the pop-up "Reopen in Container" which is shown when opening this project in VSCode.

The game is then accessible at localhost:3000/#/g/local/game.

Gitpod

You can work on this repository using Gitpod : Open in Gitpod

Note that gitpod is not setup to start the game in the background to play.

Creating a new game

In order to create a new game, click "use this template" above to create your own game. That way there is a github action that can build a docker image from your main branch which can be used to add the game to the server at adam.math.hhu.de.

stg4's People

Contributors

djvelleman avatar joneugster avatar librarianmage avatar miguelmarco avatar pitmonticone avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar

stg4's Issues

Suggestion: Family Intersection World Level 6 / 6 : Intersection of a family of unions

Thanks for these exercises!

Just a suggestion spurred by
World: Family Intersection World
Level 6 / 6 : Intersection of a family of unions

We are asked to prove:
Suppose A is a set, F and G are families of sets, and for every set s in F, A∪s∈G. Then ⋂G⊆A∪(⋂F).

example (A : Set U) (F G : Set (Set U)) (h1 : ∀ s ∈ F, A ∪ s ∈ G) : ⋂₀ G ⊆ A ∪ (⋂₀ F)

Suggestion: Either the documentation of ⋂₀ could mention, or one of the earlier levels in this world could prove, that ⋂₀ F = U when F = {} is an empty family.

Justification: It seemed to me easiest to use by_cases hxF: x ∈ ⋂₀ F to prove this, but first I had to convince myself that this included the case where F was an empty family. The added proof early in this world would help students understand this special case of the possibly unfamiliar ⋂₀ operator.

Jack

Constructor tactic missing

The constructor tactic is mentioned several times in the level descriptions (e.g. lvl5 of the intersection world). And when I use it, it indeed works as described. It is however missing from the tactic overview.:
Screenshot from 2024-07-12 21-14-57
To make the tactic more intuitively usable, it would be great if it is added to the overview.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.