define alternation depth

1 files changed, 8 insertions, 0 deletions

diff --git a/SymbolicModalLogic/MuCalculus.lean b/SymbolicModalLogic/MuCalculus.lean
index ca5b447..4722928 100644
--- a/SymbolicModalLogic/MuCalculus.lean
+++ b/SymbolicModalLogic/MuCalculus.lean
@@ -8,6 +8,14 @@ class Modalities (Λ : Type) where
   dualSignature {α : Type} : (l : Λ) → (signature l → α) → (signature (dual l) → α)
   dual_involution : ∀ l, dual (dual l) = l
 
+def Modalities.args {Λ : Type} [Modalities Λ] (l : Λ) : List (Modalities.signature l) :=
+  have : FinEnum (signature l) := Modalities.signature_finenum l
+  FinEnum.toList (signature l)
+
+def Modalities.args_mem {Λ : Type} [Modalities Λ] (l : Λ) (a : Modalities.signature l) : a ∈ args l := by
+  rw [args]
+  apply @FinEnum.mem_toList _ (Modalities.signature_finenum l)
+
 inductive Formula (Λ : Type) [Modalities Λ] where
   | top : Formula Λ
   | bot : Formula Λ