[Prev][Next][Index]

Re: LSL Latex Source



Daniel,

It isn't pretty, but here's what we used in the book.  \lsllclindent and
\key pretty much do the obvious thing.

Jim H.


%SetBasics.tex
%\begin{lsltrait}
\lsllclindent{0}
\( {\it SetBasics} ( E , C ) : \) \key{trait} 

\lsllclindent{1}
\lslcommentline{ Just the fundamental operators on sets}

\lsllclindent{1}
\key{introduces} 

\lsllclindent{2}
\( \{ \} : \rightarrow C \) 

\lsllclindent{2}
\( {\it insert} : E , C \rightarrow C \) 

\lsllclindent{2}
\( \_\_ \in \_\_ : E , C \rightarrow {\it Bool} \) 

\lsllclindent{1}
\key{asserts} 

\lsllclindent{2}
\( C \) \key{generated} \key{by} \( \{ \} , {\it insert} \) 

\lsllclindent{2}
\( C \) \key{partitioned} \key{by} \( \in \) 

\lsllclindent{2}
${\bf \forall}$ \( s : C , e , e_1 , e_2 : E \) 

\lsllclindent{3}
\( \neg ( e \in \{ \} ) \) 

\lsllclindent{3}
\( e_1 \in {\it insert} ( e_2 , s ) == e_1 = e_2 \vee e_1 \in s \) 

\lsllclindent{1}
\key{implies} 

\lsllclindent{2}
\( {\it Container} ( \{ \} \) \key{for} \( {\it empty} ) \) 

\lsllclindent{2}
${\bf \forall}$ \( e , e_1 , e_2 : E , s : C \) 

\lsllclindent{3}
\( {\it insert} ( e , s ) \neq \{ \} \) 

\lsllclindent{3}
\( {\it insert} ( e , {\it insert} ( e , s ) ) == {\it insert} ( e , s ) \)


\lsllclindent{2}
\key{converts} \( \in \) 

%\end{lsltrait}