phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
387 Commits 19 Branches 10 Tags
e7842bce82b8e1a0d75e3348d1bfa13dac337a3b
Commit Graph
105 Commits
Author SHA1 Message Date
Alexander Bentkamp bf2315b474 remove references to testgame on the server, add gameId to router 2023-03-23 16:23:06 +01:00
Jon Eugster d0b7838564 add display names for definitions and lemmas 2023-03-16 13:23:10 +01:00
Alexander Bentkamp b0d9816ce6 simpler solution to remove indented lines 2023-03-15 17:41:52 +01:00
Alexander Bentkamp 86302522a5 add atomic to fix interpolatedStr issue 2023-03-15 17:02:43 +01:00
Alexander Bentkamp 07ec94b7c2 fix strinterpolation again 2023-03-15 12:32:19 +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 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 07b5c22dda allow initial white space in hints 2023-03-10 15:30:38 +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
Alexander Bentkamp 97fd51686f basic inline hints 2023-03-10 10:09:26 +01:00
Jon Eugster b30a14caf0 do not check Doc for disabled Tactic/Lemma/Definition 2023-03-08 10:34:52 +01:00
Jon Eugster 93d05c9703 rename [New/Only/Disabled][Tactic/Lemma/Definition] 2023-03-08 09:30:01 +01:00
Jon Eugster 75f356f4b2 Add World introduction and change layout 2023-03-06 18:07:09 +01:00
Alexander Bentkamp e8b6770bab display level conclusion 2023-03-06 09:55:39 +01:00
Alexander Bentkamp ff0adf12c8 fix metavariable issue 2023-03-03 16:30:25 +01:00
Alexander Bentkamp 3cbb4774f1 hints with variable names 2023-03-03 15:55:32 +01:00
Jon Eugster 02db8617f6 add 'fun' keyword to allowed tactics 2023-03-03 12:07:22 +01:00
Jon Eugster c679325c46 exclude 'only' keyword from forbidden tactics 2023-03-03 11:22:58 +01:00
Alexander Bentkamp a783e1dffc Add tabs for lemmas #23 2023-03-02 12:15:34 +01:00
Alexander Bentkamp 7748eefa4a fix lemma check 
Fixes #36
 2023-03-02 10:25:34 +01:00
Alexander Bentkamp a44efef7de add definitions 2023-03-01 17:31:58 +01:00
Alexander Bentkamp 9a97b569b5 unify code for tactics and lemmas 2023-03-01 17:14:01 +01:00
Alexander Bentkamp 676560a0df revert to use isDefEq for hints 2023-03-01 14:41:29 +01:00
Alexander Bentkamp bc6c4a57e7 treat simp? and simp! like simp 2023-03-01 11:37:34 +01:00
Alexander Bentkamp bf7c68d4f9 pass lemma/tactic status to file worker 2023-03-01 11:20:32 +01:00
Alexander Bentkamp a85f40541e custom unification for hint trigger 2023-03-01 10:38:02 +01:00
Alexander Bentkamp 604e6757ec Import only specific Level file 
Fixes #35
 2023-02-28 13:03:46 +01:00
Alexander Bentkamp 591423b308 make opening namespaces work properly 2023-02-24 16:37:40 +01:00
Alexander Bentkamp 82af2ded8e Speed up loading by process queue #15 2023-02-23 10:18:02 +01:00
Alexander Bentkamp 09137c7019 remove set_option tactic.hygienic false 2023-02-22 17:55:46 +01:00
Alexander Bentkamp 404062c015 Use local scope from level file in game 
Fixes #31
 2023-02-22 17:45:08 +01:00
Alexander Bentkamp 1f0d9aea43 check if tactic doc exists 
Fixes #34
 2023-02-22 15:10:46 +01:00
Alexander Bentkamp f17246f6d4 check lemma names 2023-02-22 11:44:13 +01:00
Alexander Bentkamp 116026428f show lemma and tactic docs 2023-02-09 15:34:37 +01:00
Alexander Bentkamp 6e8a47b1a7 lemma inventory 2023-02-09 13:25:52 +01:00
Alexander Bentkamp c628d0eec4 new tactic display 2023-02-09 13:25:52 +01:00
Alexander Bentkamp c93f6bfc15 allow "rcases with" tactic 2023-02-09 13:25:52 +01:00
Alexander Bentkamp cd27b2026c OnlyTactics command #16 2023-02-06 15:31:26 +01:00
Alexander Bentkamp 51f82cf9eb disabled tactics command #16 2023-02-06 14:59:41 +01:00
Alexander Bentkamp a4987f14cf forbidden tactics error message #16 2023-02-06 12:25:27 +01:00
Alexander Bentkamp 76d1a08948 compute which tactics are available in which level 2023-02-03 17:04:09 +01:00
Alexander Bentkamp 03faa3ffed fix lean server error 2023-02-03 16:39:47 +01:00
Alexander Bentkamp d1eee327dd graph algos 2023-02-03 16:29:16 +01:00