From df2fa4a798f2828cbba6f6bbf39f83fc3203712e Mon Sep 17 00:00:00 2001
From: rsoeldner <r.soeldner@gmail.com>
Date: Wed, 3 Jan 2024 08:37:46 +0100
Subject: [PATCH] Add additional comment on optional syntax

---
 Manual/Description/definitions.stex | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Manual/Description/definitions.stex b/Manual/Description/definitions.stex
index fc867efe43..a0cde8f87d 100644
--- a/Manual/Description/definitions.stex
+++ b/Manual/Description/definitions.stex
@@ -2036,10 +2036,12 @@ one writes
 \end{verbatim}
 where, as with other special syntaxes, the keywords (\ml{Inductive} and \ml{End}) have to be in the leftmost column of the source file.
 Additionally, users can automatically export each rule as a theorem by assigning a name using the square-bracket syntax.
-The appropriate format is \holtxt{[\(\sim\)Name:]}, where \holtxt{Name} acts as the placeholder for the rule name, see the following example:
+The appropriate format is \holtxt{[\textasciitilde Name:]}, where \holtxt{Name} acts as the placeholder for the rule name.
+Inside the square brackets, the tilde (\textasciitilde) is optional; if included, it prefixes the exported rule name with \ml{<stem>\_}.
+For instance, the following example will export rules as \ml{rule1} and \ml{foo\_rule2}.
 \begin{verbatim}
    Inductive foo:
-   [~rule1:]
+   [rule1:]
      ...
    [~rule2:]
      ...