Commit Graph

305 Commits (ef8815f30617e79cfba4909ffd7aadd620dbcad8)

Author SHA1 Message Date
Jon Eugster c2b298e650 fix 2 years ago
Jon Eugster e93e480f27 move Statement further down in the document 2 years ago
Jon Eugster b6b4251d5d text 2 years ago
Jon Eugster 9b25eda668 levels and custom induction 2 years ago
Jon Eugster f02e591c37 typo 2 years ago
Jon Eugster b6066f5163 Merge branch 'main' of github.com:leanprover-community/lean4game 2 years ago
Jon Eugster 96a8da9d93
Apply suggestions from code review 2 years ago
Marcus Zibrowius e947c434a8 konsequente Kleinschreibung von du, dein, dir 2 years ago
Marcus Zibrowius 23abcaf488 Titelseite überarbeiten 2 years ago
Jon Eugster 0e5891371a levels 2 years ago
Jon Eugster 62fb4f52bd implement functionality of OnlyTactic 2 years ago
Jon Eugster 2e4161ca7a typos 2 years ago
Jon Eugster b8eccf3a8e
Merge branch 'main' into main 2 years ago
Jon Eugster f46b59163b add .gitignore for nng 2 years ago
Jon Eugster 85f0a2e559 use LemmaTab in levels 2 years ago
Jon Eugster 3cbe336ccb add command LemmaTab to specify default tab when loading level 2 years ago
Jon Eugster 2b1384d6a6 remove nng build data 2 years ago
Marcus Zibrowius e907c1fd5e planet names as titles for the first chapters 2 years ago
Marcus Zibrowius 11a8352fd3 story für Contradiction überarbeiten 2 years ago
Marcus Zibrowius a4c2dcb12b rewrite story for Predicate (continued) 2 years ago
Marcus Zibrowius 750e2bde32 rewrite story for Predicate 2 years ago
Jon Eugster 4ae7e0eab6 levels 2 years ago
Marcus Zibrowius 62d2e0918c rewrite story for Implication 2 years ago
Marcus Zibrowius 8cd674661d link to project website on front page 2 years ago
Marcus Zibrowius 71904d5460 merge necessary as upstream developed while storyline slept 2 years ago
Jon Eugster 4d1d97a164 nng 2 years ago
Jon Eugster 6e8911e5da add NNG 2 years ago
Jon Eugster 6cd71c93fe fix doc string 2 years ago
Alexander Bentkamp bbe38ddc7c rename testgame to adam, part 2 2 years ago
Alexander Bentkamp 5c73d3bddb rename testgame to adam 2 years ago
Jon Eugster a262cff63b Merge branch 'main' of github.com:leanprover-community/lean4game 2 years ago
Jon Eugster 6cb53965c2 levels 2 years ago
Alexander Bentkamp dac15d84b5 add build mechanism for nng 2 years ago
Alexander Bentkamp 7992cffa26 add minimal NNG dummy 2 years ago
Alexander Bentkamp bf2315b474 remove references to `testgame` on the server, add gameId to router 2 years ago
Jon Eugster a4623a8241 css 2 years ago
Jon Eugster 10a12a8e77 lemma docs and levels 2 years ago
Alexander Bentkamp a4d1130487 refine_struct 2 years ago
Jon Eugster 83ee409f47 levels 2 years ago
Jon Eugster ae58652fa9 lemma docs 2 years ago
Jon Eugster c947ef20d7 lemma docs 2 years ago
Jon Eugster 5dd846f168 levels 2 years ago
Jon Eugster 0cd416f303 tactic documentation 2 years ago
Jon Eugster c883265776 levels 2 years ago
Jon Eugster d0b7838564 add display names for definitions and lemmas 2 years ago
Jon Eugster 9480090cb4 nothin of importance 2 years ago
Jon Eugster 7382b3a77b nothing of importance 2 years ago
Jon Eugster 32a17ed9e8 storytime 2 years ago
Alexander Bentkamp b0d9816ce6 simpler solution to remove indented lines 2 years ago
Alexander Bentkamp 86302522a5 add atomic to fix interpolatedStr issue 2 years ago
Marcus Zibrowius 588c362aa3 merge 2 years ago
Alexander Bentkamp 07ec94b7c2 fix strinterpolation again 2 years ago
Jon Eugster 27e82378d0 bump mathlib and fixes 2 years ago
Jon Eugster 421606aaed story contradiction 2 years ago
Jon Eugster 93114620c4 story world 2 and 3 2 years ago
Alexander Bentkamp 18f16bfe1c disabled applies only to current level
Fixes #48
2 years ago
Alexander Bentkamp a876b71d85 fix strinterpolation 2 years ago
Jon Eugster cad766d553 Merge branch 'main' of github.com:leanprover-community/lean4game 2 years ago
Jon Eugster 3ff3c7eb69 story world 2 2 years ago
Jon Eugster 6d93aa4752 make statement description optional 2 years ago
Alexander Bentkamp 66f506c5b2 more elegant this way 2 years ago
Alexander Bentkamp 07b5c22dda allow initial white space in hints 2 years ago
Jon Eugster 7c2b1b0482 update world 1 2 years ago
Alexander Bentkamp 27532a7688 fix errors during merge 2 years ago
Alexander Bentkamp c8c85195d7 Branch 2 years ago
Alexander Bentkamp b3a38ee080 strict and hidden options 2 years ago
Alexander Bentkamp 625e224d1e hide internal Hint log messages 2 years ago
Alexander Bentkamp b0d3da99bc reimplement matchDecls 2 years ago
Alexander Bentkamp 1d7facd8dd use fvars instead of mvars for hints 2 years ago
Jon Eugster 725d27e345 Add test: Function level 10 2 years ago
Alexander Bentkamp f540b63764 test example 2 years ago
Alexander Bentkamp 97fd51686f basic inline hints 2 years ago
Jon Eugster 04bba0220d levels 2 years ago
Jon Eugster ae82567b2d story 2 years ago
Jon Eugster 41a2b52ac3 levels: Function 2 years ago
Jon Eugster 7dde866039 levels 2 years ago
Jon Eugster b30a14caf0 do not check Doc for disabled Tactic/Lemma/Definition 2 years ago
Jon Eugster 93d05c9703 rename [New/Only/Disabled][Tactic/Lemma/Definition] 2 years ago
Marcus Zibrowius fc493635d1 merge with upstream 2 years ago
Marcus Zibrowius ef5f39fef0 minor edits 2 years ago
Jon Eugster 01199c3793 levels Function 2 years ago
Jon Eugster 0987e3751c levels 2 years ago
Jon Eugster 21e98fa81e change titles to german for now 2 years ago
Jon Eugster 75f356f4b2 Add World introduction and change layout 2 years ago
Jon Eugster cdea03781c levels 2 years ago
Jon Eugster 6d67459e08 story for first world 2 years ago
Jon Eugster 6987b4cb01 levels 2 years ago
Alexander Bentkamp 874999ed34 show summary permanently 2 years ago
Alexander Bentkamp c35b66a0c6 use hints for initial texts 2 years ago
Alexander Bentkamp 4158283eb3 Merge branch 'main' into story 2 years ago
Alexander Bentkamp e8b6770bab display level conclusion 2 years ago
Alexander Bentkamp 2d96279203 make it compile 2 years ago
Marcus Zibrowius b33febfadd story line for planet 1 2 years ago
Jon Eugster 6644fc6431 text 2 years ago
Alexander Bentkamp 5af93f0a2a Improve texts 2 years ago
Alexander Bentkamp e6c481a9a4 a few examples of the new feature 2 years ago
Alexander Bentkamp ff0adf12c8 fix metavariable issue 2 years ago
Alexander Bentkamp 86f3e07b27 fix escaping issue 2 years ago
Alexander Bentkamp 3cbb4774f1 hints with variable names 2 years ago
Jon Eugster 02db8617f6 add 'fun' keyword to allowed tactics 2 years ago