Demo : parse ↔

hferee · Sep 12, 2024 · 9d3758e · 9d3758e
1 parent 54426f8
commit 9d3758e
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git 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
@@ -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>