[Prev][Next][Index]
Re: LSL Latex Source
-
To: "Daniel Schweizer" <schweizer@tik.ethz.ch>
-
Subject: Re: LSL Latex Source
-
From: horning
-
Date: Mon, 12 Jun 95 16:08:22 -0700
-
Cc: horning
-
Delivery-Date: Mon, 12 Jun 95 16:08:26 -0700
-
In-Reply-To: Message of 6 Jun 1995 18:07:00 +0200
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}