Commit 44813a5f authored by Glen Mével's avatar Glen Mével
Browse files

add in spec of queue that \isQueue is objective

parent 8da74c0a
\begin{figure}
\[\small\begin{array}{@{}l@{}}
\infer{~}{\persistent{\queueInv}}
\qquad
\infer{~}{\objective{\isQueue \tview \hview \elemViewList}}
\\\\\\
\hoareV
{\seen\view_0}
{\make~\Unit}
{\Lam \queue. \Exists \gqueue.
\queueInv
\isep \isQueue {\view_0} {\view_0} {[]}
\isep \persistent{\queueInv}
}
\\\\\\
......
......@@ -323,6 +323,9 @@
% lifting a formula from iProp to vProp:
\newcommand{\liftobj}[1]{\lceil#1\rceil}
% pure fact that an assertion is objective:
\newcommand{\objective}[1]{\textlog{objective}(#1)}
% access modes:
\newcommand{\accmodeNA}{\textrm{na}}
\newcommand{\accmodeAT}{\textrm{at}}
......
Supports Markdown
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