import Mathlib.Tactic everywhere

2023-08-04 17:14:49 +02:00
parent 827fe844f4
commit 836f8f6078
11 changed files with 48 additions and 22 deletions
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -19,8 +19,14 @@ open Lean in
  modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
   : Elab.Command.CommandElabM Unit)

+-- require mathlib from git
+--   "https://github.com/leanprover-community/mathlib4" @ "88e129706828e01b7622d6635af1ca6667e25bac"
+
+-- `Game` fix:
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4" @ "88e129706828e01b7622d6635af1ca6667e25bac"
+  "https://github.com/leanprover-community/mathlib4" @ "b04c509ef69fc7939b5f67715a635e15743dbe3c"
+
+

 package Game where
  moreLeanArgs := #["-Dtactic.hygienic=false"]