Merge pull request #86 from katydid/update_lean_411r2

update lean to 4.11rc2

.github/workflows/check_proofs.yml

@@ -22,7 +22,7 @@ jobs:
         run: |
           curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
           chmod u+x elan-init.sh
-          ./elan-init.sh -y --default-toolchain leanprover/lean4:v4.2.0-rc4
+          ./elan-init.sh -y --default-toolchain leanprover/lean4:v4.11.0-rc2
           echo "Adding location $HOME/.elan/bin to PATH..."
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 

Katydid/Std/Balistic.lean

@@ -6,6 +6,10 @@ open Qq
 
 -- balistic is a tactic that tries to solve simple theorems about lists
 
+-- This temporarily fixes matching exists using quote4 in wreck_exists
+-- see https://github.com/leanprover-community/quote4/issues/52
+set_option linter.constructorNameAsVariable false
+
 -- TODO: incorporate ac_rfl into balistic
 -- ac_rfl uses IsAssociative to prove associativity of operators
 example (xs ys zs: List α): (xs ++ ys ++ zs) = (xs ++ ys) ++ zs := by

lake-manifest.json

@@ -1,19 +1,21 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
-   "name": "std",
+   "scope": "leanprover-community",
+   "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "scope": "leanprover-community",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,56 +24,52 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c",
+   "scope": "leanprover-community",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "scope": "leanprover-community",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3",
+   "scope": "leanprover-community",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "19b5ded3c60a6da7b357a126fb56b56671d231e3",
+   "scope": "",
+   "rev": "cae1b27ace5330f372b57f1051e228fe9b264d57",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/forked-from-1kasper/ground_zero",
-   "type": "git",
-   "subDir": null,
-   "rev": "a3122579f48dc7aa9a65be33d218249569980327",
-   "name": "GroundZero",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "katydid",
  "lakeDir": ".lake"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.11.0-rc2