From 67d2268d7861490baeb5e393c97c3e66ff93b5e6 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 10:24:15 -0700 Subject: [PATCH] refactor(Core/Logic): cut RestrictedModality's import inversion into Semantics --- Linglib/Core/Logic/Intensional/RestrictedModality.lean | 1 - Linglib/Semantics/Modality/EventRelativity.lean | 1 + Linglib/Semantics/Modality/Kratzer/Flavor.lean | 1 + Linglib/Studies/Tsiakmakis2025.lean | 1 + 4 files changed, 3 insertions(+), 1 deletion(-) diff --git a/Linglib/Core/Logic/Intensional/RestrictedModality.lean b/Linglib/Core/Logic/Intensional/RestrictedModality.lean index 41129aee4..3e146f7a9 100644 --- a/Linglib/Core/Logic/Intensional/RestrictedModality.lean +++ b/Linglib/Core/Logic/Intensional/RestrictedModality.lean @@ -1,7 +1,6 @@ import Linglib.Core.Logic.Intensional.Defs import Linglib.Core.Logic.Intensional.Quantification import Linglib.Core.Logic.Intensional.Algebra -import Linglib.Semantics.Modality.ModalTypes import Mathlib.Data.Finset.Basic import Mathlib.Data.Fintype.Basic import Mathlib.Order.Lattice diff --git a/Linglib/Semantics/Modality/EventRelativity.lean b/Linglib/Semantics/Modality/EventRelativity.lean index e72c0674e..dafd47119 100644 --- a/Linglib/Semantics/Modality/EventRelativity.lean +++ b/Linglib/Semantics/Modality/EventRelativity.lean @@ -1,4 +1,5 @@ import Linglib.Core.Logic.Intensional.RestrictedModality +import Linglib.Semantics.Modality.ModalTypes /-! # Event-Relative Modality diff --git a/Linglib/Semantics/Modality/Kratzer/Flavor.lean b/Linglib/Semantics/Modality/Kratzer/Flavor.lean index 6c32f6c95..db620a875 100644 --- a/Linglib/Semantics/Modality/Kratzer/Flavor.lean +++ b/Linglib/Semantics/Modality/Kratzer/Flavor.lean @@ -8,6 +8,7 @@ modal base and ordering source for different types of modality. -/ import Linglib.Semantics.Modality.Kratzer.Operators +import Linglib.Semantics.Modality.ModalTypes namespace Semantics.Modality.Kratzer diff --git a/Linglib/Studies/Tsiakmakis2025.lean b/Linglib/Studies/Tsiakmakis2025.lean index d2852f219..9796df392 100644 --- a/Linglib/Studies/Tsiakmakis2025.lean +++ b/Linglib/Studies/Tsiakmakis2025.lean @@ -1,5 +1,6 @@ import Linglib.Studies.JinKoenig2021 import Linglib.Semantics.Modality.Kratzer.Operators +import Linglib.Semantics.Modality.ModalTypes import Linglib.Fragments.Greek.StandardModern.Negation import Linglib.Fragments.Italian.Negation import Mathlib.Data.Fin.Basic