From d63be9758d9d83bc9320bed4ab73a81c92c815e4 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sat, 20 Jun 2026 15:57:49 +0200 Subject: start formalizing alternation depth --- SymbolicModalLogic/Instances/Relational.lean | 1 + 1 file changed, 1 insertion(+) (limited to 'SymbolicModalLogic/Instances/Relational.lean') diff --git a/SymbolicModalLogic/Instances/Relational.lean b/SymbolicModalLogic/Instances/Relational.lean index 4c9155b..81d428d 100644 --- a/SymbolicModalLogic/Instances/Relational.lean +++ b/SymbolicModalLogic/Instances/Relational.lean @@ -4,6 +4,7 @@ import SymbolicModalLogic.MuCalculus inductive Relational where | box | diamond + deriving Repr namespace Relational -- cgit v1.3.1