phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
382 Commits 19 Branches 10 Tags
cbc9576f98372645ecdd371805aa146a1e443a6c
Commit Graph
113 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
Jon Eugster 27e82378d0 bump mathlib and fixes 2023-03-15 12:08:50 +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
Jon Eugster 695903f5d8 Merge branch 'main' of github.com:leanprover-community/lean4game 2023-02-27 10:40:50 +01:00
Alexander Bentkamp 591423b308 make opening namespaces work properly 2023-02-24 16:37:40 +01:00
Jon Eugster c065dcc5e3 Merge branch 'main' of github.com:leanprover-community/lean4game 2023-02-24 14:43:41 +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
Jon Eugster 51f111bbed bump mathlib 2023-02-14 12:07:33 +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