From 375b241c6fe701e69c92a691a90f56439baa9cb9 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Sat, 30 Nov 2024 21:22:04 +0000 Subject: [PATCH] Version bump --- DeBruijnSSA/BinSyntax/SimpleTyping.lean | 1 - DeBruijnSSA/BinSyntax/Typing/BBRegion/Basic.lean | 1 - DeBruijnSSA/BinSyntax/Typing/Block/Basic.lean | 1 - DeBruijnSSA/BinSyntax/Typing/Body/Basic.lean | 1 - DeBruijnSSA/BinSyntax/Typing/Ctx.lean | 3 +-- DeBruijnSSA/BinSyntax/Typing/LCtx.lean | 1 - DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean | 1 - DeBruijnSSA/BinSyntax/Typing/TRegion/Basic.lean | 1 - DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean | 1 - DeBruijnSSA/BinSyntax/Typing/Terminator/Basic.lean | 1 - DeBruijnSSA/BinSyntax/Typing/Ty.lean | 2 +- DeBruijnSSA/InstSet.lean | 2 +- lake-manifest.json | 10 +++++----- lean-toolchain | 2 +- 14 files changed, 9 insertions(+), 19 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/SimpleTyping.lean b/DeBruijnSSA/BinSyntax/SimpleTyping.lean index 957c3c0..04c8536 100644 --- 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 index 74826db..1de722e 100644 --- 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 index 3198cfc..deda78f 100644 --- 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 index cc31ab4..a7134e7 100644 --- 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 index b937a1f..48d9a91 100644 --- 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 index 1ec68bc..51f48ba 100644 --- 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 index 4e1cc34..d7c5066 100644 --- 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 index b8920f6..c781f3f 100644 --- 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 index aaf3a1e..c5daa30 100644 --- 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 index bb01d98..b2a99b4 100644 --- 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 index ef299a5..e1d6f6a 100644 --- 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 index 67013ad..661f78a 100644 --- 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 index d766e46..5572007 100644 --- 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 index 57a4710..6d9e70f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc2 +leanprover/lean4:v4.14.0-rc3