restructureHEADmain

8 files changed, 126 insertions, 105 deletions

diff --git a/CoalgebraicMuCalculus.lean b/CoalgebraicMuCalculus.lean
new file mode 100644
index 0000000..e58c455
--- /dev/null
+++ b/CoalgebraicMuCalculus.lean
@@ -0,0 +1,3 @@
+import CoalgebraicMuCalculus.FixedPoints
+import CoalgebraicMuCalculus.MuCalculus
+import CoalgebraicMuCalculus.Instances.Relational
diff --git a/SymbolicModalLogic/AlternationDepth.lean b/CoalgebraicMuCalculus/AlternationDepth.lean
index 717c928..fae628d 100644
--- a/SymbolicModalLogic/AlternationDepth.lean
+++ b/CoalgebraicMuCalculus/AlternationDepth.lean
@@ -1,4 +1,4 @@
-import SymbolicModalLogic.MuCalculus
+import CoalgebraicMuCalculus.MuCalculus
 import Mathlib
 
 inductive FixedPointOp where
diff --git a/SymbolicModalLogic/FixedPoints.lean b/CoalgebraicMuCalculus/FixedPoints.lean
index 58d768c..58d768c 100644
--- a/SymbolicModalLogic/FixedPoints.lean
+++ b/CoalgebraicMuCalculus/FixedPoints.lean
diff --git a/SymbolicModalLogic/Instances/Relational.lean b/CoalgebraicMuCalculus/Instances/Relational.lean
index 81d428d..0b0f7fc 100644
--- a/SymbolicModalLogic/Instances/Relational.lean
+++ b/CoalgebraicMuCalculus/Instances/Relational.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import SymbolicModalLogic.MuCalculus
+import CoalgebraicMuCalculus.MuCalculus
 
 inductive Relational where
   | box
diff --git a/SymbolicModalLogic/MuCalculus.lean b/CoalgebraicMuCalculus/MuCalculus.lean
index 4722928..5d4cab9 100644
--- a/SymbolicModalLogic/MuCalculus.lean
+++ b/CoalgebraicMuCalculus/MuCalculus.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import SymbolicModalLogic.FixedPoints
+import CoalgebraicMuCalculus.FixedPoints
 
 class Modalities (Λ : Type) where
   signature : Λ → Type
diff --git a/SymbolicModalLogic.lean b/SymbolicModalLogic.lean
deleted file mode 100644
index dd1d18a..0000000
--- a/SymbolicModalLogic.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import SymbolicModalLogic.FixedPoints
-import SymbolicModalLogic.MuCalculus
-import SymbolicModalLogic.Instances.Relational
diff --git a/lake-manifest.json b/lake-manifest.json
index 190adef..fc5713b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,96 +1,117 @@
-{"version": "1.2.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/plausible",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
-   "name": "plausible",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
-   "name": "LeanSearchClient",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
-   "name": "importGraph",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
-   "name": "proofwidgets",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.99",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
-   "name": "Qq",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
-   "inherited": true,
-   "configFile": "lakefile.toml"}],
- "name": "SymbolicModalLogic",
- "lakeDir": ".lake",
- "fixedToolchain": false}
+{
+  "version": "1.2.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "url": "https://github.com/leanprover-community/mathlib4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
+      "name": "mathlib",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.30.0",
+      "inherited": false,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+      "name": "LeanSearchClient",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
+      "name": "importGraph",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+      "name": "proofwidgets",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v0.0.99",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+      "name": "aesop",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.30.0",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+      "name": "Qq",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.30.0",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "32dc18cde3684679f3c003de608743b57498c56f",
+      "name": "batteries",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.30.0",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    }
+  ],
+  "name": "CoalgebraicMuCalculus",
+  "lakeDir": ".lake",
+  "fixedToolchain": false
+}
\ No newline at end of file
diff --git a/lakefile.toml b/lakefile.toml
index d6fcfd6..5730c3f 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,6 +1,6 @@
-name = "SymbolicModalLogic"
+name = "CoalgebraicMuCalculus"
 version = "0.1.0"
-defaultTargets = ["SymbolicModalLogic"]
+defaultTargets = ["CoalgebraicMuCalculus"]
 
 [[require]]
 name = "mathlib"
@@ -8,4 +8,4 @@ scope = "leanprover-community"
 rev = "v4.30.0"
 
 [[lean_lib]]
-name = "SymbolicModalLogic"
+name = "CoalgebraicMuCalculus"