diff options
Diffstat (limited to 'SymbolicModalLogic/MuCalculus.lean')
| -rw-r--r-- | SymbolicModalLogic/MuCalculus.lean | 8 |
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 Λ |