From 9d3758e33aea974371e9b8bb237a1d35b01f6052 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= <feree@irif.fr>
Date: Thu, 12 Sep 2024 20:21:55 +0200
Subject: [PATCH] =?UTF-8?q?Demo=20:=20parse=20=E2=86=94?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 bin/modal_expressions_parser.ml | 5 ++++-
 doc-config/resources/demo.html  | 4 ++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/bin/modal_expressions_parser.ml b/bin/modal_expressions_parser.ml
index 1593c6c..3b6d9ea 100644
--- a/bin/modal_expressions_parser.ml
+++ b/bin/modal_expressions_parser.ml
@@ -22,7 +22,10 @@ let disj = spaces *> ((char '\xE2' *> char '\x88' *> char '\xA8') <|> char '|')
 let conj = spaces *> ((char '\xE2' *> char '\x88' *> char '\xA7') <|> char '&') *> spaces *> return (fun x y -> And (x, y))
 
 let modal (p : form t) : form t = box p <|> neg p <|> diamond p
-let impl = spaces *> ((char '\xE2' *> char '\x86' *> char '\x92') <|> (char '-' *> char '>')) *> spaces *> return (fun x y -> Implies(x, y))
+let impl = spaces *> ((char '\xE2' *> char '\x86' *> char '\x92') <|> (char '-' *> char '>')) *> spaces *>
+  return (fun x y -> Implies(x, y))
+let iff = spaces *> ((char '\xE2' *> char '\x86' *> char '\x94') <|> (char '<' *> char '-' *> char '>')) *> spaces *>
+  return (fun x y -> And(Implies(x, y), Implies(y, x)))
 
 (* this is ⊥ *)
 let bot = spaces *> ((char '\xE2' *> char '\x8A' *> char '\xA5') <|> char '#'
diff --git a/doc-config/resources/demo.html b/doc-config/resources/demo.html
index c94d08f..15a2038 100644
--- a/doc-config/resources/demo.html
+++ b/doc-config/resources/demo.html
@@ -72,6 +72,10 @@
           <td>implication</td>
         </tr>
         <tr>
+          <td>↔</td>
+          <td class="ms"><-></td>
+          <td>equivalence</td>
+        </tr>       <tr>
           <td>¬</td>
           <td class="ms">~</td>
           <td>negation</td>