summaryrefslogtreecommitdiff
path: root/SymbolicModalLogic/Instances
diff options
context:
space:
mode:
authorHannes Schulze <contact@haschu.me>2026-06-20 15:57:49 +0200
committerHannes Schulze <contact@haschu.me>2026-06-20 15:57:49 +0200
commitd63be9758d9d83bc9320bed4ab73a81c92c815e4 (patch)
treeecd59301ca036ab65b80c273de44d9c2ea7972bc /SymbolicModalLogic/Instances
parentaa03bb5570c2d0189b6606b7b42a52c302f6fe5f (diff)
start formalizing alternation depth
Diffstat (limited to 'SymbolicModalLogic/Instances')
-rw-r--r--SymbolicModalLogic/Instances/Relational.lean1
1 files changed, 1 insertions, 0 deletions
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