phc
/
lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Commit Graph

  • 01199c3793 levels Function Jon Eugster 2023-03-07 17:13:32 +0100
  • 0987e3751c levels Jon Eugster 2023-03-07 14:49:26 +0100
  • ff7d8d5f5e sort Inventories Jon Eugster 2023-03-07 11:48:58 +0100
  • f6f2d6e1bd Merge branch 'main' of github.com:leanprover-community/lean4game Jon Eugster 2023-03-07 11:09:22 +0100
  • 21e98fa81e change titles to german for now Jon Eugster 2023-03-07 11:08:50 +0100
  • d71f43b854 hide hidden hints again when goal changes Alexander Bentkamp 2023-03-07 09:25:57 +0100
  • 1c3fa815da fix bug: level completed on reload Alexander Bentkamp 2023-03-07 08:59:23 +0100
  • 75f356f4b2 Add World introduction and change layout Jon Eugster 2023-03-06 18:07:09 +0100
  • cdea03781c levels Jon Eugster 2023-03-06 16:30:43 +0100
  • 6d67459e08 story for first world Jon Eugster 2023-03-06 14:40:39 +0100
  • 6987b4cb01 levels Jon Eugster 2023-03-06 11:29:44 +0100
  • a01212e3ca Merge branch 'story' Alexander Bentkamp 2023-03-06 12:38:32 +0100
  • 874999ed34 show summary permanently #43 Alexander Bentkamp 2023-03-06 10:19:45 +0100
  • 1c7169d34a show buttons on level completion Alexander Bentkamp 2023-03-06 10:17:41 +0100
  • c35b66a0c6 use hints for initial texts Alexander Bentkamp 2023-03-06 10:04:40 +0100
  • 4158283eb3 Merge branch 'main' into story Alexander Bentkamp 2023-03-06 09:55:57 +0100
  • e8b6770bab display level conclusion Alexander Bentkamp 2023-03-06 09:55:39 +0100
  • 2d96279203 make it compile Alexander Bentkamp 2023-03-06 09:46:22 +0100
  • b33febfadd story line for planet 1 Marcus Zibrowius 2023-03-05 18:43:59 +0100
  • 6644fc6431 text Jon Eugster 2023-03-03 17:26:59 +0100
  • 5af93f0a2a Improve texts Alexander Bentkamp 2023-03-03 17:00:05 +0100
  • a42841ba97 small css issues Alexander Bentkamp 2023-03-03 16:48:56 +0100
  • e6c481a9a4 a few examples of the new feature Alexander Bentkamp 2023-03-03 16:36:13 +0100
  • ff0adf12c8 fix metavariable issue Alexander Bentkamp 2023-03-03 16:30:25 +0100
  • 86f3e07b27 fix escaping issue Alexander Bentkamp 2023-03-03 15:58:17 +0100
  • 3cbb4774f1 hints with variable names Alexander Bentkamp 2023-03-03 15:55:15 +0100
  • 02db8617f6 add 'fun' keyword to allowed tactics Jon Eugster 2023-03-03 12:07:22 +0100
  • 99080aa5ff levels up to 'Lean' Jon Eugster 2023-03-03 11:54:37 +0100
  • c679325c46 exclude 'only' keyword from forbidden tactics Jon Eugster 2023-03-03 11:22:58 +0100
  • c015d1e1f9 edit package.json to run lake build once at startup Jon Eugster 2023-03-03 10:46:11 +0100
  • a783e1dffc Add tabs for lemmas #23 Alexander Bentkamp 2023-03-02 12:15:34 +0100
  • 7748eefa4a fix lemma check Alexander Bentkamp 2023-03-02 10:25:18 +0100
  • c7bf92c168 levels Jon Eugster 2023-03-01 18:39:43 +0100
  • a44efef7de add definitions Alexander Bentkamp 2023-03-01 17:31:44 +0100
  • 2be1a348ee Merge branch 'main' of github.com:leanprover-community/lean4game Jon Eugster 2023-03-01 17:25:42 +0100
  • a18582a5f8 levels Jon Eugster 2023-03-01 17:25:10 +0100
  • 9a97b569b5 unify code for tactics and lemmas Alexander Bentkamp 2023-03-01 17:14:01 +0100
  • 676560a0df revert to use isDefEq for hints Alexander Bentkamp 2023-03-01 14:41:29 +0100
  • 0ebf890392 levels Jon Eugster 2023-03-01 11:56:01 +0100
  • aca781879a edit package.json Jon Eugster 2023-03-01 11:55:44 +0100
  • bc6c4a57e7 treat `simp?` and `simp!` like `simp` Alexander Bentkamp 2023-03-01 11:37:34 +0100
  • bf7c68d4f9 pass lemma/tactic status to file worker Alexander Bentkamp 2023-03-01 11:20:32 +0100
  • 4f93dbf928 disable automatic compilation of lean files Alexander Bentkamp 2023-03-01 10:55:03 +0100
  • a85f40541e custom unification for hint trigger Alexander Bentkamp 2023-03-01 10:38:02 +0100
  • bc7533d18f loading icon for loading goals Alexander Bentkamp 2023-02-28 14:37:14 +0100
  • 604e6757ec Import only specific Level file Alexander Bentkamp 2023-02-28 13:03:31 +0100
  • 8a9b1a25e8 levels Jon Eugster 2023-02-27 12:20:01 +0100
  • 695903f5d8 Merge branch 'main' of github.com:leanprover-community/lean4game Jon Eugster 2023-02-27 10:40:50 +0100
  • cbd1867148 levels Jon Eugster 2023-02-27 10:40:46 +0100
  • 591423b308 make opening namespaces work properly Alexander Bentkamp 2023-02-24 16:37:40 +0100
  • c065dcc5e3 Merge branch 'main' of github.com:leanprover-community/lean4game Jon Eugster 2023-02-24 14:43:41 +0100
  • 5921de848d Preload all files in a world #15 Alexander Bentkamp 2023-02-23 17:11:11 +0100
  • 82af2ded8e Speed up loading by process queue #15 Alexander Bentkamp 2023-02-23 10:18:02 +0100
  • 09137c7019 remove `set_option tactic.hygienic false` Alexander Bentkamp 2023-02-22 17:55:46 +0100
  • 404062c015 Use local scope from level file in game Alexander Bentkamp 2023-02-22 17:45:08 +0100
  • 49f9ff035f fix version of lean4 infoview Alexander Bentkamp 2023-02-22 15:48:46 +0100
  • 1f0d9aea43 check if tactic doc exists Alexander Bentkamp 2023-02-22 15:10:46 +0100
  • f17246f6d4 check lemma names Alexander Bentkamp 2023-02-22 11:44:13 +0100
  • 06f4f4e223 typo Alexander Bentkamp 2023-02-22 11:40:59 +0100
  • 45b13fa959 levels Jon Eugster 2023-02-17 16:12:56 +0100
  • ebfd31a111 bump mathlib Jon Eugster 2023-02-15 11:55:14 +0100
  • 51f111bbed bump mathlib Jon Eugster 2023-02-14 12:07:33 +0100
  • e4d5010163 Merge branch 'main' of github.com:leanprover-community/lean4game Jon Eugster 2023-02-13 17:48:18 +0100
  • af3afc3a94 levels Jon Eugster 2023-02-13 17:48:11 +0100
  • 02ac370a62 Run -> Execute Alexander Bentkamp 2023-02-09 15:48:52 +0100
  • 84ce05a548 more styling Alexander Bentkamp 2023-02-09 15:42:10 +0100
  • 116026428f show lemma and tactic docs Alexander Bentkamp 2023-02-09 15:34:37 +0100
  • 891d51829c rename leftpanel to inventory Alexander Bentkamp 2023-02-09 14:26:57 +0100
  • 622aca644e correct shrinking of command line Alexander Bentkamp 2023-02-09 13:54:06 +0100
  • ca329a933c make command line look the same on all browsers Alexander Bentkamp 2023-02-09 13:43:59 +0100
  • 6e8a47b1a7 lemma inventory Alexander Bentkamp 2023-02-09 13:25:40 +0100
  • c628d0eec4 new tactic display Alexander Bentkamp 2023-02-08 17:06:15 +0100
  • c93f6bfc15 allow "rcases with" tactic Alexander Bentkamp 2023-02-08 13:11:01 +0100
  • e264f11d60 inventory experiment Alexander Bentkamp 2023-02-07 21:14:29 +0100
  • 992781ba11 css Jon Eugster 2023-02-08 16:39:54 +0100
  • 2e73bc3330 css Jon Eugster 2023-02-08 16:16:14 +0100
  • abcc3087d3 new levels Jon Eugster 2023-02-08 16:05:51 +0100
  • 6d1058773c move excercise to middle panel. Jon Eugster 2023-02-08 16:05:28 +0100
  • e20613901f Merge branch 'main' of github.com:leanprover-community/lean4game Jon Eugster 2023-02-08 10:34:47 +0100
  • 07b140acf7 levels Jon Eugster 2023-02-08 10:33:45 +0100
  • 7510b83591 hide command line in "other goals" Alexander Bentkamp 2023-02-07 16:03:04 +0100
  • 278aedb20c more monaco command line Alexander Bentkamp 2023-02-07 15:39:40 +0100
  • a3b1011035 monaco command line Alexander Bentkamp 2023-02-07 13:25:57 +0100
  • cd27b2026c OnlyTactics command #16 Alexander Bentkamp 2023-02-06 15:31:26 +0100
  • 51f82cf9eb disabled tactics command #16 Alexander Bentkamp 2023-02-06 14:59:41 +0100
  • dd4fe60f7e update package json Alexander Bentkamp 2023-02-06 14:24:30 +0100
  • a4987f14cf forbidden tactics error message #16 Alexander Bentkamp 2023-02-06 12:25:27 +0100
  • 76d1a08948 compute which tactics are available in which level Alexander Bentkamp 2023-02-03 17:04:09 +0100
  • 03faa3ffed fix lean server error Alexander Bentkamp 2023-02-03 16:39:47 +0100
  • 85a96579a5 remove tactic set for real Alexander Bentkamp 2023-02-03 16:31:56 +0100
  • d1eee327dd graph algos Alexander Bentkamp 2023-02-03 16:29:16 +0100
  • 3f433507db remove TacticSet command Alexander Bentkamp 2023-02-02 14:51:12 +0100
  • ad50fb986d bump mathlib Jon Eugster 2023-02-02 16:05:58 +0100
  • f0171797f3 typo Jon Eugster 2023-02-02 14:58:55 +0100
  • 72d65824b1 Merge branch 'main' of github.com:leanprover-community/lean4game Jon Eugster 2023-02-02 14:45:48 +0100
  • 404f346920 set theory levels Jon Eugster 2023-02-02 14:44:58 +0100
  • 41cc23543b fix command line bug Alexander Bentkamp 2023-02-02 09:35:03 +0100
  • 73a44bd057 disable undo button Alexander Bentkamp 2023-01-30 15:30:48 +0100
  • 5025fa939b show line numbers only in editor mode Alexander Bentkamp 2023-01-30 15:18:06 +0100
  • 45f88cf5a8 undo button Alexander Bentkamp 2023-01-30 15:15:39 +0100