summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CoalgebraicMuCalculus.lean3
-rw-r--r--CoalgebraicMuCalculus/AlternationDepth.lean (renamed from SymbolicModalLogic/AlternationDepth.lean)2
-rw-r--r--CoalgebraicMuCalculus/FixedPoints.lean (renamed from SymbolicModalLogic/FixedPoints.lean)0
-rw-r--r--CoalgebraicMuCalculus/Instances/Relational.lean (renamed from SymbolicModalLogic/Instances/Relational.lean)2
-rw-r--r--CoalgebraicMuCalculus/MuCalculus.lean (renamed from SymbolicModalLogic/MuCalculus.lean)2
-rw-r--r--SymbolicModalLogic.lean3
-rw-r--r--lake-manifest.json213
-rw-r--r--lakefile.toml6
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"
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 10:19:57 +0000