bump to v4.5.0
This commit is contained in:
@@ -1,6 +1,6 @@
|
|||||||
import Mathlib.Lean.Expr.Basic
|
import Mathlib.Lean.Expr.Basic
|
||||||
import Lean.Elab.Tactic.Basic
|
import Lean.Elab.Tactic.Basic
|
||||||
-- import Lean.Elab.Tactic.Rewrite
|
import Lean.Elab.Tactic.Rewrite
|
||||||
|
|
||||||
/-!
|
/-!
|
||||||
# Modified `rw`
|
# Modified `rw`
|
||||||
|
|||||||
@@ -4,25 +4,25 @@
|
|||||||
[{"url": "https://github.com/leanprover/std4.git",
|
[{"url": "https://github.com/leanprover/std4.git",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "af7f36db6e7e9e395710a70635f915e8e3a0e69b",
|
"rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
|
||||||
"name": "std",
|
"name": "std",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v4.4.0",
|
"inputRev": "v4.5.0",
|
||||||
"inherited": true,
|
"inherited": true,
|
||||||
"configFile": "lakefile.lean"},
|
"configFile": "lakefile.lean"},
|
||||||
{"url": "https://github.com/leanprover-community/lean4game.git",
|
{"url": "https://github.com/leanprover-community/lean4game.git",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": "server",
|
"subDir": "server",
|
||||||
"rev": "e579071a3b1f0fd48146acf68e186a7270b557aa",
|
"rev": "3b660c518505b8f677224e3e36d1940d20ccb4bc",
|
||||||
"name": "GameServer",
|
"name": "GameServer",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v4.4.0",
|
"inputRev": "v4.5.0",
|
||||||
"inherited": false,
|
"inherited": false,
|
||||||
"configFile": "lakefile.lean"},
|
"configFile": "lakefile.lean"},
|
||||||
{"url": "https://github.com/leanprover-community/quote4",
|
{"url": "https://github.com/leanprover-community/quote4",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
|
"rev": "1c88406514a636d241903e2e288d21dc6d861e01",
|
||||||
"name": "Qq",
|
"name": "Qq",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "master",
|
"inputRev": "master",
|
||||||
@@ -31,7 +31,7 @@
|
|||||||
{"url": "https://github.com/leanprover-community/aesop",
|
{"url": "https://github.com/leanprover-community/aesop",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "646be3a3604d0f2a3c1800cb4279a36493474b18",
|
"rev": "cebd10ba6d22457e364ba03320cfd9fc7511e520",
|
||||||
"name": "aesop",
|
"name": "aesop",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "master",
|
"inputRev": "master",
|
||||||
@@ -40,10 +40,10 @@
|
|||||||
{"url": "https://github.com/leanprover-community/ProofWidgets4",
|
{"url": "https://github.com/leanprover-community/ProofWidgets4",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
|
"rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
|
||||||
"name": "proofwidgets",
|
"name": "proofwidgets",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v0.0.23",
|
"inputRev": "v0.0.25",
|
||||||
"inherited": true,
|
"inherited": true,
|
||||||
"configFile": "lakefile.lean"},
|
"configFile": "lakefile.lean"},
|
||||||
{"url": "https://github.com/leanprover/lean4-cli",
|
{"url": "https://github.com/leanprover/lean4-cli",
|
||||||
@@ -55,13 +55,22 @@
|
|||||||
"inputRev": "main",
|
"inputRev": "main",
|
||||||
"inherited": true,
|
"inherited": true,
|
||||||
"configFile": "lakefile.lean"},
|
"configFile": "lakefile.lean"},
|
||||||
|
{"url": "https://github.com/leanprover-community/import-graph.git",
|
||||||
|
"type": "git",
|
||||||
|
"subDir": null,
|
||||||
|
"rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
|
||||||
|
"name": "importGraph",
|
||||||
|
"manifestFile": "lake-manifest.json",
|
||||||
|
"inputRev": "main",
|
||||||
|
"inherited": true,
|
||||||
|
"configFile": "lakefile.lean"},
|
||||||
{"url": "https://github.com/leanprover-community/mathlib4.git",
|
{"url": "https://github.com/leanprover-community/mathlib4.git",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "cf8e23a62939ed7cc530fbb68e83539730f32f86",
|
"rev": "feec58a7ee9185f92abddcf7631643b53181a7d3",
|
||||||
"name": "mathlib",
|
"name": "mathlib",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v4.4.0",
|
"inputRev": "v4.5.0",
|
||||||
"inherited": false,
|
"inherited": false,
|
||||||
"configFile": "lakefile.lean"}],
|
"configFile": "lakefile.lean"}],
|
||||||
"name": "Game",
|
"name": "Game",
|
||||||
|
|||||||
@@ -1 +1 @@
|
|||||||
leanprover/lean4:v4.4.0
|
leanprover/lean4:v4.5.0
|
||||||
|
|||||||
Reference in New Issue
Block a user