From 2774094c061a147a4e62d90b6b3bc7fdc5263ae9 Mon Sep 17 00:00:00 2001
From: giopaglia <24519853+giopaglia@users.noreply.github.com>
Date: Fri, 21 Jul 2023 05:27:51 +0200
Subject: [PATCH] global_diamond, global_box

---
 src/SoleLogics.jl  | 2 ++
 src/modal-logic.jl | 6 ++++--
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/SoleLogics.jl b/src/SoleLogics.jl
index ca62670c..9a5362e3 100644
--- a/src/SoleLogics.jl
+++ b/src/SoleLogics.jl
@@ -69,6 +69,8 @@ export AbstractWorldSet, WorldSet
 
 export Interval, Interval2D, OneWorld
 
+export global_diamond, global_box
+
 include("modal-logic.jl")
 
 export LeftmostLinearForm, LeftmostConjunctiveForm, LeftmostDisjunctiveForm, Literal
diff --git a/src/modal-logic.jl b/src/modal-logic.jl
index 00d38fb3..95c39275 100644
--- a/src/modal-logic.jl
+++ b/src/modal-logic.jl
@@ -973,10 +973,12 @@ See also
 dual(op::DiamondRelationalOperator) = BoxRelationalOperator{relationtype(op)}()
 dual(op::BoxRelationalOperator)     = DiamondRelationalOperator{relationtype(op)}()
 
+global_diamond = DiamondRelationalOperator(globalrel)
+global_box = BoxRelationalOperator(globalrel)
 
 const BASE_MULTIMODAL_OPERATORS = [BASE_PROPOSITIONAL_OPERATORS...,
-    DiamondRelationalOperator(globalrel),
-    BoxRelationalOperator(globalrel),
+    global_diamond,
+    global_box,
     DiamondRelationalOperator(identityrel),
     BoxRelationalOperator(identityrel),
 ]