Skip to content
Snippets Groups Projects
Commit 05806a4b authored by Thomas Muller's avatar Thomas Muller
Browse files

Added info about the Type Environment View.

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@14611 1434b563-b632-4741-aa49-43a3a8374d2e
parent 5cbe1b2f
Branches
No related tags found
No related merge requests found
org.rodinp.handbook.feature/latex/img/reference/ref_01_proving_perspective15.png

17.4 KiB

......@@ -728,6 +728,18 @@ This window allows the user to keep track of recently manipulated (i.e. used, re
Operations similar to those in the \textsf{Selected Hypotheses} and \textsf{Search Hypotheses} views are also available for the cached hypotheses. It is possible to remove, select, and start a proof by contradiction (\icon{rodin/falsify_prover.png}) in the \textsf{Cache Hypotheses} view as well. Interactive proof steps (e.g., rewriting) can also be carried out in the \textsf{Cache Hypotheses} view.
\subsection{The Type Environment View}
\begin{figure}[!ht]
\begin{center}
\includegraphics{img/reference/ref_01_proving_perspective15.png}
\caption{Proof Information View}
\label{fig_ref_01_proving_perspective15}
\end{center}
\end{figure}
This view~\ref{fig_ref_01_proving_perspective15} shows the type environment for the current node of the proof (free identifiers and their type). It is accessible through \textsf{Window} $ \rangle $ \textsf{Show View} $ \rangle $ \textsf{Type Environment}.
\subsubsection{Proof Information View}
This view displays information so that the user can relate a proof obligation to the model. For example, typical information for an event invariant preservation includes the event as well as the invariant in question. For instance, in Figure \ref{fig_ref_01_proving_perspective8}, the hyperlinks \textsf{CreateToken} and \textsf{inv2} can be used to navigate to the containing machine.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment