From e635d2acc874704839b41d0e4ddecc97fd4b1dd7 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 14 Jul 2026 20:00:07 +0200 Subject: define alternation depth --- SymbolicModalLogic/MuCalculus.lean | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'SymbolicModalLogic/MuCalculus.lean') 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 Λ -- cgit v1.3.1