From cc5837f526d1b7c5d5e1af5a9d4c89a39a7cd257 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Wed, 11 Oct 2023 18:20:22 +0200
Subject: [PATCH] adjust notation

---
 Pdl/Syntax.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Pdl/Syntax.lean b/Pdl/Syntax.lean
index aaba74b..a172b75 100644
--- a/Pdl/Syntax.lean
+++ b/Pdl/Syntax.lean
@@ -53,8 +53,8 @@ notation "⊥" => Formula.bottom
 notation "⊤" => Formula.neg Formula.bottom
 infixr:66 "⋀" => Formula.and
 infixr:60 "⋁" => Formula.or
-infixr:55 "↣" => fun φ ψ => ~φ⋀(~ψ)
-infixl:77 "⟷" => fun ϕ ψ => (ϕ↣ψ)⋀(ψ↣ϕ)
+notation:55 φ:56 " ↣ " ψ:55 => ~φ ⋀ (~ψ)
+notation:55 φ:56 " ⟷ " ψ:55 => (φ↣ψ) ⋀ (φ↣φ)
 notation "⌈" α "⌉" P => Formula.box α P -- TOOD: adjust precedence to make ⌈α⌉⌈β⌉P work, or is it fine already?
 prefix:33 "†" => Formula.nstar