Tap

imbrem · Aug 2, 2024 · 4a07268 · 4a07268
1 parent bc6bfa5
commit 4a07268
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 10 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean b/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean
@@ -591,6 +591,7 @@ theorem lsubst_ucfg {n : ℕ} {β : Region φ} {G : Fin n → Region φ} {ρ : S
   congr
   funext k
   simp only [cfgSubst, Subst.comp]
+  sorry
 
 -- theorem lwk_ucfg {n : ℕ} {β : Region φ} {G : Fin n → Region φ}
 --   : (ucfg n β G).lwk ρ = ucfg n (β.lwk (Nat.liftnWk n ρ)) (λi => (G i).lwk (Nat.liftnWk n ρ)) := by

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d2b1546c5fc05a06426e3f6ee1cb020e71be5592",
+   "rev": "41bc768e2224d6c75128a877f1d6e198859b3178",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
+   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.40",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cc495260156b40dcbd55b947c047061e15344000",
+   "rev": "2df7d9446f22706562263d8b55076dc073e10d02",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c7d1ce74de32273b0cac8f07a4732d50414f1fe2",
+   "rev": "bbfc62e71f35b8ebaad4f73b13210e0a9b8474a8",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.10.0
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.10.0-rc2
		leanprover/lean4:v4.10.0