Add Example.lean for matrix operations and update dependencies to v4.29.0-rc6

Author: HEIGE-PCloud

ProgramAnalysis/ProbabilisticPrograms/Example.lean

@@ -0,0 +1,7 @@
+import Mathlib.Data.Matrix.Basic
+
+def matrix1 : Matrix (Fin 2) (Fin 3) Nat := ![![1, 2, 3], ![4, 5, 6]]
+def matrix2 : Matrix (Fin 3) (Fin 2) Nat := ![![1, 2], ![3, 4], ![5, 6]]
+
+#eval matrix1
+#eval matrix1 * matrix2

lake-manifest.json

@@ -5,27 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
+   "rev": "58f63c64f7207514bdd291f66d1b67e62e6f8a20",
    "name": "mathlib4",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "78a9bfe6b811fece2e00bf2c92e30729eeb8dc4e",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
+   "rev": "e84e3e16aea6b72cc5d311ca1bb25caad417e162",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
+   "rev": "f207d9fcf0cef00ba79962a33ef156061914d9c7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
+   "rev": "2e58165a9dcdca9837b666528f974299ee1a51cc",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.87",
+   "inputRev": "v0.0.92",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
+   "rev": "c3361708f266893de5d1769192b60d4b1831f2bb",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,20 +65,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
+   "rev": "221e8088e3a066b8676dc471ff10638cf1c10835",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "77a5160a74772214ef37caba2847cfe9ab600285",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
+   "rev": "3de531c1135f5e3a01f3ac04830996fda476b28e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0",
+   "inputRev": "v4.29.0-rc6",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "ProgramAnalysis",

lakefile.toml

@@ -9,12 +9,6 @@ name = "ProgramAnalysis"
 name = "programanalysis"
 root = "Main"
 
-[[require]]
-name = "batteries"
-scope = "leanprover-community"
-rev = "main"
-
 [[require]]
 name = "mathlib4"
-scope = "leanprover-community"
-rev = "v4.28.0"
+scope = "leanprover-community"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.28.0
+leanprover/lean4:v4.29.0-rc6