Version bump

imbrem · Sep 16, 2024 · 402288e · 402288e
1 parent 78c0337
commit 402288e
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 7 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
@@ -58,13 +58,13 @@ theorem Subst.InS.liftn_append_congr {Γ : Ctx α ε} {L K J : LCtx α}
     simp only [Set.mem_setOf_eq, List.get_eq_getElem]
     congr 3
     rw [List.getElem_append_right _ _ h']
-    apply heq_prop
+    apply proof_irrel_heq
     congr 1
     funext r
     simp only [Set.mem_setOf_eq, List.get_eq_getElem]
     congr 3
     rw [List.getElem_append_right _ _ h']
-    apply heq_prop
+    apply proof_irrel_heq
 
 theorem Subst.InS.slift_congr {Γ : Ctx α ε} {L K : LCtx α}
   {σ τ : Subst.InS φ Γ L K} (h : σ ≈ τ) : σ.slift (head := head) ≈ τ.slift

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
+   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
+   "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,17 +55,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8ab24d4bb8b4c4a52af3f39027f255b1901669c9",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3e18f1777d9adc6889ce44a51a451bbd54e691aa",
+   "rev": "1b1a09185ee9ffb73f8161f42fdf7ceebf507a94",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7cc792161e8a2752c79b224d1c7627b70d8105e7",
+   "rev": "64879d94466c15f3832a5eb1e85efbdc7956d2da",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",