phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
363 Commits 19 Branches 10 Tags
86302522a54eb01b8d407aea571ebc0c15667122
Commit Graph
363 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
Alexander Bentkamp 86302522a5 add atomic to fix interpolatedStr issue 2023-03-15 17:02:43 +01:00
Alexander Bentkamp f2eed5fc0c repair command line 2023-03-15 16:55:50 +01:00
Alexander Bentkamp 07ec94b7c2 fix strinterpolation again 2023-03-15 12:32:19 +01:00
Jon Eugster 27e82378d0 bump mathlib and fixes 2023-03-15 12:08:50 +01:00
Jon Eugster 421606aaed story contradiction 2023-03-15 11:19:18 +01:00
Jon Eugster 93114620c4 story world 2 and 3 2023-03-14 10:38:10 +01:00
Alexander Bentkamp 18f16bfe1c disabled applies only to current level 
Fixes #48
 2023-03-13 13:53:31 +01:00
Alexander Bentkamp a876b71d85 fix strinterpolation 2023-03-13 12:24:05 +01:00
Jon Eugster cad766d553 Merge branch 'main' of github.com:leanprover-community/lean4game 2023-03-13 10:08:40 +01:00
Jon Eugster 3ff3c7eb69 story world 2 2023-03-10 19:40:16 +01:00
Jon Eugster 6d93aa4752 make statement description optional 2023-03-10 17:10:05 +01:00
Alexander Bentkamp 66f506c5b2 more elegant this way 2023-03-10 16:37:04 +01:00
Alexander Bentkamp 481f2b5cbb refactor level code 2023-03-10 16:20:02 +01:00
Alexander Bentkamp 35eb6c3ec0 refactor LevelAppBar 2023-03-10 16:11:11 +01:00
Alexander Bentkamp 5dfa7b56ec doc panel 2023-03-10 15:48:22 +01:00
Alexander Bentkamp 07b5c22dda allow initial white space in hints 2023-03-10 15:30:38 +01:00
Jon Eugster 7c2b1b0482 update world 1 2023-03-10 15:14:07 +01:00
Alexander Bentkamp 27532a7688 fix errors during merge 2023-03-10 10:14:51 +01:00
Alexander Bentkamp c8c85195d7 Branch 2023-03-10 10:11:36 +01:00
Alexander Bentkamp b3a38ee080 strict and hidden options 2023-03-10 10:11:36 +01:00
Alexander Bentkamp 625e224d1e hide internal Hint log messages 2023-03-10 10:11:36 +01:00
Alexander Bentkamp b0d3da99bc reimplement matchDecls 2023-03-10 10:11:36 +01:00
Alexander Bentkamp 1d7facd8dd use fvars instead of mvars for hints 2023-03-10 10:11:36 +01:00
Jon Eugster 725d27e345 Add test: Function level 10 2023-03-10 10:11:36 +01:00
Alexander Bentkamp f540b63764 test example 2023-03-10 10:10:55 +01:00
Alexander Bentkamp 97fd51686f basic inline hints 2023-03-10 10:09:26 +01:00
Jon Eugster 04bba0220d levels 2023-03-09 17:10:17 +01:00
Jon Eugster ae82567b2d story 2023-03-09 17:02:42 +01:00
Jon Eugster 41a2b52ac3 levels: Function 2023-03-08 20:10:51 +01:00
Jon Eugster 7dde866039 levels 2023-03-08 16:33:14 +01:00
Jon Eugster 1145f8dd0b Merge branch 'main' of github.com:leanprover-community/lean4game 2023-03-08 10:35:22 +01:00
Jon Eugster b30a14caf0 do not check Doc for disabled Tactic/Lemma/Definition 2023-03-08 10:34:52 +01:00
Alexander Bentkamp 3f39db59ab Update NOTES.md 2023-03-08 10:13:58 +01:00
Jon Eugster 93d05c9703 rename [New/Only/Disabled][Tactic/Lemma/Definition] 2023-03-08 09:30:01 +01:00
Jon Eugster 01199c3793 levels Function 2023-03-07 17:13:32 +01:00
Jon Eugster 0987e3751c levels 2023-03-07 14:49:26 +01:00
Jon Eugster ff7d8d5f5e sort Inventories 2023-03-07 11:48:58 +01:00
Jon Eugster f6f2d6e1bd Merge branch 'main' of github.com:leanprover-community/lean4game 2023-03-07 11:09:22 +01:00
Jon Eugster 21e98fa81e change titles to german for now 2023-03-07 11:08:50 +01:00
Alexander Bentkamp d71f43b854 hide hidden hints again when goal changes 2023-03-07 09:25:57 +01:00
Alexander Bentkamp 1c3fa815da fix bug: level completed on reload 2023-03-07 08:59:48 +01:00
Jon Eugster 75f356f4b2 Add World introduction and change layout 2023-03-06 18:07:09 +01:00
Jon Eugster cdea03781c levels 2023-03-06 16:30:43 +01:00
Jon Eugster 6d67459e08 story for first world 2023-03-06 14:40:39 +01:00
Jon Eugster 6987b4cb01 levels 2023-03-06 12:39:28 +01:00
Alexander Bentkamp a01212e3ca Merge branch 'story' 2023-03-06 12:38:32 +01:00
Alexander Bentkamp 874999ed34 show summary permanently 2023-03-06 10:19:45 +01:00
Alexander Bentkamp 1c7169d34a show buttons on level completion 2023-03-06 10:17:41 +01:00
Alexander Bentkamp c35b66a0c6 use hints for initial texts 2023-03-06 10:04:40 +01:00
Alexander Bentkamp 4158283eb3 Merge branch 'main' into story 2023-03-06 09:55:57 +01:00