Commit 3a5fe7b5 authored by Allan Blanchard's avatar Allan Blanchard

[wp/doc] Document tactic: Validity

parent 9176cd9e
......@@ -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 \\
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment