From 26972b2523481c8e5d113a9e6f9853a20241cd2d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?St=C3=A9phane=20Del=20Pino?= <stephane.delpino44@gmail.com>
Date: Tue, 24 May 2022 19:03:54 +0200
Subject: [PATCH] Add doc for string comparison operators

---
 doc/userdoc.org | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/doc/userdoc.org b/doc/userdoc.org
index 207e283d6..d2abb3de6 100644
--- a/doc/userdoc.org
+++ b/doc/userdoc.org
@@ -1407,6 +1407,20 @@ they follow a few rules.
       \right.
     \end{equation*}
   #+end_src
+\\
+  This is also the case for ~string~ values: only allowed operators are
+  ~==~ and ~!=~.
+  #+begin_src latex :results drawer :exports results
+    \begin{equation*}
+      \left|
+        \begin{array}{rl}
+          \mathtt{==}:& \mathtt{string} \times \mathtt{string} \to \mathbb{B}\\
+          \mathtt{!=}:& \mathtt{string} \times \mathtt{string} \to \mathbb{B}
+        \end{array}
+      \right.
+    \end{equation*}
+  #+end_src
+
 - Shift operators ~<<~ and ~>>~ are not used to define binary operators
   between two basic types
 - Arithmetic operators are defined
-- 
GitLab