From 3a5fe7b5333c2ec37136c5a3b1a4f47f0af4768b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 5 Nov 2020 08:23:44 +0100
Subject: [PATCH] [wp/doc] Document tactic: Validity
---
src/plugins/wp/doc/manual/wp_plugin.tex | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index b89ca18abd9..8b30530ca66 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -378,6 +378,12 @@ Finally, when the user select a arithmetic comparison over $a$ and $b$, the tact
\Delta,a>b&\models G
\end{array}} \]
+\paragraph{Validity} Unfold validity and range definitions\\
+The user selects a validity expression (\lstinline{valid_rd},
+\lstinline{valid_rw}, \lstinline{invalid} or \lstinline{included}).
+The expression is unfolded to a \textsf{Qed} term.
+
+
\subsubsection{Over integers}
\paragraph{BitRange} Range of logical bitwise operators \\
--
GitLab