Version bump

imbrem · Nov 30, 2024 · 375b241 · 375b241
1 parent 1474a97
commit 375b241
Show file tree

Hide file tree

Showing 14 changed files with 9 additions and 19 deletions.
diff --git a/DeBruijnSSA/BinSyntax/SimpleTyping.lean b/DeBruijnSSA/BinSyntax/SimpleTyping.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions
 import DeBruijnSSA.BinSyntax.Typing

diff --git a/DeBruijnSSA/BinSyntax/Typing/BBRegion/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/BBRegion/Basic.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions

diff --git a/DeBruijnSSA/BinSyntax/Typing/Block/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Block/Basic.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions

diff --git a/DeBruijnSSA/BinSyntax/Typing/Body/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Body/Basic.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions

diff --git a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions
@@ -520,7 +519,7 @@ theorem Var.wk_res (h : V ≤ V') (hΓ : Γ.Var n V) : Γ.Var n V' where
   length := hΓ.length
   getElem := le_trans hΓ.get h
 
-theorem Var.wk_res₂ (hA : A ≤ A') (he : e ≤ e') (hΓ : Γ.Var n ⟨A, e⟩) : Γ.Var n ⟨A', e⟩
+theorem Var.wk_res₂ (hA : A ≤ A') (he : e ≤ e') (hΓ : Γ.Var n ⟨A, e⟩) : Γ.Var n ⟨A', e'⟩
   := hΓ.wk_res (by simp [hA, he])
 
 theorem Var.wk_ty (h : A ≤ A') (hΓ : Γ.Var n ⟨A, e⟩) : Γ.Var n ⟨A', e⟩

diff --git a/DeBruijnSSA/BinSyntax/Typing/LCtx.lean b/DeBruijnSSA/BinSyntax/Typing/LCtx.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions

diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions

diff --git a/DeBruijnSSA/BinSyntax/Typing/TRegion/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/TRegion/Basic.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions

diff --git a/DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import Discretion.Utils.Set
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic

diff --git a/DeBruijnSSA/BinSyntax/Typing/Terminator/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Terminator/Basic.lean
@@ -1,5 +1,4 @@
 import Discretion.Wk.List
-import Discretion.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions

diff --git a/DeBruijnSSA/BinSyntax/Typing/Ty.lean b/DeBruijnSSA/BinSyntax/Typing/Ty.lean
@@ -1,6 +1,6 @@
 
 import Discretion.Wk.List
-import Discretion.Basic
+import Discretion.Order.Discrete
 import DeBruijnSSA.BinSyntax.Syntax.Definitions
 import DeBruijnSSA.BinSyntax.Syntax.Fv.Basic
 import DeBruijnSSA.BinSyntax.Syntax.Effect.Definitions

diff --git a/DeBruijnSSA/InstSet.lean b/DeBruijnSSA/InstSet.lean
@@ -1,5 +1,5 @@
 import Mathlib.Order.Monotone.Basic
-import Mathlib.Order.BoundedOrder
+import Mathlib.Order.BoundedOrder.Basic
 import Mathlib.Data.Bool.Basic
 import Mathlib.Order.Lattice
 import Mathlib.Data.Set.Basic

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
+   "rev": "f46c0445cc86ad2bc973edf8c5b2bd88bd91913b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
+   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "12a4321786fd0be1ddbe12701a45920a519b2108",
+   "rev": "4fafb9f5b76af48f96d2366beee76af2113161f7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "789f3b88b7030aad77e26c3bd8a938bfe5f87b0c",
+   "rev": "955b94eb753e7952bf657109073b92e26fe5f455",
    "name": "discretion",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

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