From 02cc3fb4d702577005ce83be6034facde31111a4 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Wed, 2 Jul 2025 04:15:16 +0000 Subject: [PATCH 1/6] Remove unnecessary imports from multiple Lean files Co-authored-by: kim --- LeroyCompilerVerificationCourse/Compil.lean | 2 -- LeroyCompilerVerificationCourse/Constprop.lean | 1 - LeroyCompilerVerificationCourse/Deadcode.lean | 1 - LeroyCompilerVerificationCourse/Fixpoints.lean | 3 --- 4 files changed, 7 deletions(-) diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean index dd68bd6..d4f6188 100644 --- a/LeroyCompilerVerificationCourse/Compil.lean +++ b/LeroyCompilerVerificationCourse/Compil.lean @@ -1,6 +1,4 @@ -import LeroyCompilerVerificationCourse.Sequences import LeroyCompilerVerificationCourse.Imp -import Init.Data.List.Basic set_option grind.warning false diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean index eff2afa..c7cdf55 100644 --- a/LeroyCompilerVerificationCourse/Constprop.lean +++ b/LeroyCompilerVerificationCourse/Constprop.lean @@ -1,4 +1,3 @@ -import LeroyCompilerVerificationCourse.Sequences import LeroyCompilerVerificationCourse.Imp import Init.Data.List.Basic import Std.Data.HashMap diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean index 37d55cd..af380eb 100644 --- a/LeroyCompilerVerificationCourse/Deadcode.lean +++ b/LeroyCompilerVerificationCourse/Deadcode.lean @@ -1,4 +1,3 @@ -import LeroyCompilerVerificationCourse.Sequences import LeroyCompilerVerificationCourse.Imp import Init.Data.List.Basic import Std.Data.HashSet diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean index 96f7fd4..90315fb 100644 --- a/LeroyCompilerVerificationCourse/Fixpoints.lean +++ b/LeroyCompilerVerificationCourse/Fixpoints.lean @@ -5,9 +5,6 @@ import Std.Data.HashMap import Std.Data.HashMap.Lemmas import Batteries.Data.List.Basic import Batteries.Data.List.Perm -import Init.Data.List.Pairwise -import Init.Data.List.Sublist -import Init.Data.List.Basic universe u From 2a2b017d3bae4614460cef25bf70f28e0290c573 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Wed, 2 Jul 2025 04:25:18 +0000 Subject: [PATCH 2/6] Remove unnecessary imports from various Lean files Co-authored-by: kim --- LeroyCompilerVerificationCourse.lean | 1 - LeroyCompilerVerificationCourse/Constprop.lean | 2 -- LeroyCompilerVerificationCourse/Deadcode.lean | 2 -- LeroyCompilerVerificationCourse/Fixpoints.lean | 2 -- 4 files changed, 7 deletions(-) diff --git a/LeroyCompilerVerificationCourse.lean b/LeroyCompilerVerificationCourse.lean index 8fa57b2..59a28df 100644 --- a/LeroyCompilerVerificationCourse.lean +++ b/LeroyCompilerVerificationCourse.lean @@ -5,4 +5,3 @@ import LeroyCompilerVerificationCourse.Compil import LeroyCompilerVerificationCourse.Constprop import LeroyCompilerVerificationCourse.Deadcode import LeroyCompilerVerificationCourse.Fixpoints -import LeroyCompilerVerificationCourse.Sequences diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean index c7cdf55..5e41f7a 100644 --- a/LeroyCompilerVerificationCourse/Constprop.lean +++ b/LeroyCompilerVerificationCourse/Constprop.lean @@ -1,7 +1,5 @@ import LeroyCompilerVerificationCourse.Imp -import Init.Data.List.Basic import Std.Data.HashMap -import Std.Data.HashMap.Lemmas open Classical in instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where beq m n := Id.run do diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean index af380eb..081d42f 100644 --- a/LeroyCompilerVerificationCourse/Deadcode.lean +++ b/LeroyCompilerVerificationCourse/Deadcode.lean @@ -1,7 +1,5 @@ import LeroyCompilerVerificationCourse.Imp -import Init.Data.List.Basic import Std.Data.HashSet -import Std.Data.HashSet.Lemmas set_option grind.warning false open Classical in diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean index 90315fb..8481651 100644 --- a/LeroyCompilerVerificationCourse/Fixpoints.lean +++ b/LeroyCompilerVerificationCourse/Fixpoints.lean @@ -2,8 +2,6 @@ import LeroyCompilerVerificationCourse.Imp import LeroyCompilerVerificationCourse.Constprop import Init.WF import Std.Data.HashMap -import Std.Data.HashMap.Lemmas -import Batteries.Data.List.Basic import Batteries.Data.List.Perm universe u From 4ea2c1462aba388487fa2d60597690f0a04ae8a3 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Wed, 2 Jul 2025 04:31:17 +0000 Subject: [PATCH 3/6] Remove unnecessary import of Init.WF Co-authored-by: kim --- LeroyCompilerVerificationCourse/Fixpoints.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean index 8481651..405bf87 100644 --- a/LeroyCompilerVerificationCourse/Fixpoints.lean +++ b/LeroyCompilerVerificationCourse/Fixpoints.lean @@ -1,6 +1,5 @@ import LeroyCompilerVerificationCourse.Imp import LeroyCompilerVerificationCourse.Constprop -import Init.WF import Std.Data.HashMap import Batteries.Data.List.Perm From 37892c1d6add9acb4559a14d83c4ad5dc000149f Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Wed, 2 Jul 2025 04:34:52 +0000 Subject: [PATCH 4/6] Remove unused imports from library modules Co-authored-by: kim --- LeroyCompilerVerificationCourse.lean | 1 - LeroyCompilerVerificationCourse/Fixpoints.lean | 1 - LeroyCompilerVerificationCourse/Imp.lean | 2 ++ 3 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LeroyCompilerVerificationCourse.lean b/LeroyCompilerVerificationCourse.lean index 59a28df..68bf44d 100644 --- a/LeroyCompilerVerificationCourse.lean +++ b/LeroyCompilerVerificationCourse.lean @@ -1,7 +1,6 @@ -- This module serves as the root of the `LeroyCompilerVerificationCourse` library. -- Import modules here that should be built as part of the library. import LeroyCompilerVerificationCourse.Imp -import LeroyCompilerVerificationCourse.Compil import LeroyCompilerVerificationCourse.Constprop import LeroyCompilerVerificationCourse.Deadcode import LeroyCompilerVerificationCourse.Fixpoints diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean index 405bf87..8c495db 100644 --- a/LeroyCompilerVerificationCourse/Fixpoints.lean +++ b/LeroyCompilerVerificationCourse/Fixpoints.lean @@ -1,6 +1,5 @@ import LeroyCompilerVerificationCourse.Imp import LeroyCompilerVerificationCourse.Constprop -import Std.Data.HashMap import Batteries.Data.List.Perm universe u diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean index f9860f9..bc685b1 100644 --- a/LeroyCompilerVerificationCourse/Imp.lean +++ b/LeroyCompilerVerificationCourse/Imp.lean @@ -1,4 +1,6 @@ + import LeroyCompilerVerificationCourse.Sequences + set_option grind.warning false def ident := String deriving BEq, Repr, Hashable From 4df110a567e8b489c30c74500441b237beffd60e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Jul 2025 06:47:08 +0200 Subject: [PATCH 5/6] Revert --- LeroyCompilerVerificationCourse.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/LeroyCompilerVerificationCourse.lean b/LeroyCompilerVerificationCourse.lean index cecc7e7..22431fe 100644 --- a/LeroyCompilerVerificationCourse.lean +++ b/LeroyCompilerVerificationCourse.lean @@ -7,6 +7,8 @@ Authors: Wojciech Różowski -- This module serves as the root of the `LeroyCompilerVerificationCourse` library. -- Import modules here that should be built as part of the library. import LeroyCompilerVerificationCourse.Imp +import LeroyCompilerVerificationCourse.Compil import LeroyCompilerVerificationCourse.Constprop import LeroyCompilerVerificationCourse.Deadcode import LeroyCompilerVerificationCourse.Fixpoints +import LeroyCompilerVerificationCourse.Sequences From 33f56ebb0bc50f61ce4c56a0ffbaf51f5d965865 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Jul 2025 06:47:34 +0200 Subject: [PATCH 6/6] . --- LeroyCompilerVerificationCourse/Deadcode.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/LeroyCompilerVerificationCourse/Deadcode.lean b/LeroyCompilerVerificationCourse/Deadcode.lean index d47c1ac..40643d9 100644 --- a/LeroyCompilerVerificationCourse/Deadcode.lean +++ b/LeroyCompilerVerificationCourse/Deadcode.lean @@ -7,8 +7,6 @@ Authors: Wojciech Różowski import LeroyCompilerVerificationCourse.Imp import Std.Data.HashSet -open Classical in - open Classical in @[grind] def IdentSet := Std.HashSet ident deriving Membership, Union, EmptyCollection