summaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-modr.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/RefMan-modr.tex')
-rw-r--r--doc/refman/RefMan-modr.tex565
1 files changed, 565 insertions, 0 deletions
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
new file mode 100644
index 00000000..b2ea232c
--- /dev/null
+++ b/doc/refman/RefMan-modr.tex
@@ -0,0 +1,565 @@
+\chapter[The Module System]{The Module System\label{chapter:Modules}}
+
+The module system extends the Calculus of Inductive Constructions
+providing a convenient way to structure large developments as well as
+a mean of massive abstraction.
+%It is described in details in Judicael's thesis and Jacek's thesis
+
+\section{Modules and module types}
+
+\paragraph{Access path.} It is denoted by $p$, it can be either a module
+variable $X$ or, if $p'$ is an access path and $id$ an identifier, then
+$p'.id$ is an access path.
+
+\paragraph{Structure element.} It is denoted by \elem\ and is either a
+definition of a constant, an assumption, a definition of an inductive,
+ a definition of a module, an alias of module or a module type abbreviation.
+
+\paragraph{Structure expression.} It is denoted by $S$ and can be:
+\begin{itemize}
+\item an access path $p$
+\item a plain structure $\struct{\nelist{\elem}{;}}$
+\item a functor $\functor{X}{S}{S'}$, where $X$ is a module variable,
+ $S$ and $S'$ are structure expression
+\item an application $S\,p$, where $S$ is a structure expression and $p$
+an access path
+\item a refined structure $\with{S}{p}{p'}$ or $\with{S}{p}{t:T}$ where $S$
+is a structure expression, $p$ and $p'$ are access paths, $t$ is a term
+and $T$ is the type of $t$.
+\end{itemize}
+
+\paragraph{Module definition,} is written $\Mod{X}{S}{S'}$ and
+ consists of a module variable $X$, a module type
+$S$ which can be any structure expression and optionally a module implementation $S'$
+ which can be any structure expression except a refined structure.
+
+\paragraph{Module alias,} is written $\ModA{X}{p}$ and
+ consists of a module variable $X$ and a module path $p$.
+
+\paragraph{Module type abbreviation,} is written $\ModType{Y}{S}$, where
+$Y$ is an identifier and $S$ is any structure expression .
+
+
+\section{Typing Modules}
+
+In order to introduce the typing system we first slightly extend
+the syntactic class of terms and environments given in
+section~\ref{Terms}. The environments, apart from definitions of
+constants and inductive types now also hold any other structure elements.
+Terms, apart from variables, constants and complex terms,
+include also access paths.
+
+We also need additional typing judgments:
+\begin{itemize}
+\item \WFT{E}{S}, denoting that a structure $S$ is well-formed,
+
+\item \WTM{E}{p}{S}, denoting that the module pointed by $p$ has type $S$ in
+environment $E$.
+
+\item \WEV{E}{S}{\overline{S}}, denoting that a structure $S$ is evaluated to
+a structure $\overline{S}$ in weak head normal form.
+
+\item \WS{E}{S_1}{S_2}, denoting that a structure $S_1$ is a subtype of a
+structure $S_2$.
+
+\item \WS{E}{\elem_1}{\elem_2}, denoting that a structure element
+ $\elem_1$ is more precise that a structure element $\elem_2$.
+\end{itemize}
+The rules for forming structures are the following:
+\begin{description}
+\item[WF-STR]
+\inference{%
+ \frac{
+ \WF{E;E'}{}
+ }{%%%%%%%%%%%%%%%%%%%%%
+ \WFT{E}{\struct{E'}}
+ }
+}
+\item[WF-FUN]
+\inference{%
+ \frac{
+ \WFT{E;\ModS{X}{S}}{\overline{S'}}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WFT{E}{\functor{X}{S}{S'}}
+ }
+}
+\end{description}
+Evaluation of structures to weak head normal form:
+\begin{description}
+\item[WEVAL-APP]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WEV{E}{S}{\functor{X}{S_1}{S_2}}~~~~~\WEV{E}{S_1}{\overline{S_1}}\\
+ \WTM{E}{p}{S_3}\qquad \WS{E}{S_3}{\overline{S_1}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WEV{E}{S\,p}{S_2\{p/X,t_1/p_1.c_1,\ldots,t_n/p_n.c_n\}}
+ }
+}
+\end{description}
+In the last rule, $\{t_1/p_1.c_1,\ldots,t_n/p_n.c_n\}$ is the resulting
+ substitution from the inlining mechanism. We substitute in $S$ the
+ inlined fields $p_i.c_i$ form $\ModS{X}{S_1}$ by the corresponding delta-reduced term $t_i$ in $p$.
+\begin{description}
+\item[WEVAL-WITH-MOD]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WEV{E}{S}{\structe{\ModS{X}{S_1}}}~~~~~\WEV{E;\elem_1;\ldots;\elem_i}{S_1}{\overline{S_1}}\\
+ \WTM{E}{p}{S_2}\qquad \WS{E;\elem_1;\ldots;\elem_i}{S_2}{\overline{S_1}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{array}{c}
+ \WEVT{E}{\with{S}{x}{p}}{\structes{\ModA{X}{p}}{p/X}}
+ \end{array}
+ }
+}
+\item[WEVAL-WITH-MOD-REC]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\
+ \WEV{E;\elem_1;\ldots;\elem_i}{\with{S_1}{p}{p_1}}{\overline{S_2}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{array}{c}
+ \WEVT{E}{\with{S}{X_1.p}{p_1}}{\structes{\ModS{X}{\overline{S_2}}}{p_1/X_1.p}}
+ \end{array}
+ }
+}
+\item[WEVAL-WITH-DEF]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WEV{E}{S}{\structe{\Assum{}{c}{T_1}}}\\
+ \WS{E;\elem_1;\ldots;\elem_i}{\Def{}{c}{t}{T}}{\Assum{}{c}{T_1}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{array}{c}
+ \WEVT{E}{\with{S}{c}{t:T}}{\structe{\Def{}{c}{t}{T}}}
+ \end{array}
+ }
+}
+\item[WEVAL-WITH-DEF-REC]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\
+ \WEV{E;\elem_1;\ldots;\elem_i}{\with{S_1}{p}{p_1}}{\overline{S_2}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{array}{c}
+ \WEVT{E}{\with{S}{X_1.p}{t:T}}{\structe{\ModS{X}{\overline{S_2}}}}
+ \end{array}
+ }
+}
+
+\item[WEVAL-PATH-MOD]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WEV{E}{p}{\structe{ \Mod{X}{S}{S_1}}}\\
+ \WEV{E;\elem_1;\ldots;\elem_i}{S}{\overline{S}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WEV{E}{p.X}{\overline{S}}
+ }
+}
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WF{E}{}~~~~~~\Mod{X}{S}{S_1}\in E\\
+ \WEV{E}{S}{\overline{S}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WEV{E}{X}{\overline{S}}
+ }
+}
+\item[WEVAL-PATH-ALIAS]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WEV{E}{p}{\structe{\ModA{X}{p_1}}}\\
+ \WEV{E;\elem_1;\ldots;\elem_i}{p_1}{\overline{S}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WEV{E}{p.X}{\overline{S}}
+ }
+}
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WF{E}{}~~~~~~~\ModA{X}{p_1}\in E\\
+ \WEV{E}{p_1}{\overline{S}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WEV{E}{X}{\overline{S}}
+ }
+}
+\item[WEVAL-PATH-TYPE]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WEV{E}{p}{\structe{\ModType{Y}{S}}}\\
+ \WEV{E;\elem_1;\ldots;\elem_i}{S}{\overline{S}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WEV{E}{p.Y}{\overline{S}}
+ }
+}
+\item[WEVAL-PATH-TYPE]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WF{E}{}~~~~~~~\ModType{Y}{S}\in E\\
+ \WEV{E}{S}{\overline{S}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WEV{E}{Y}{\overline{S}}
+ }
+}
+\end{description}
+ Rules for typing module:
+\begin{description}
+\item[MT-EVAL]
+\inference{%
+ \frac{
+ \WEV{E}{p}{\overline{S}}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WTM{E}{p}{\overline{S}}
+ }
+}
+\item[MT-STR]
+\inference{%
+ \frac{
+ \WTM{E}{p}{S}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WTM{E}{p}{S/p}
+ }
+}
+\end{description}
+The last rule, called strengthening is used to make all module fields
+manifestly equal to themselves. The notation $S/p$ has the following
+meaning:
+\begin{itemize}
+\item if $S\lra\struct{\elem_1;\dots;\elem_n}$ then
+ $S/p=\struct{\elem_1/p;\dots;\elem_n/p}$ where $\elem/p$ is defined as
+ follows:
+ \begin{itemize}
+ \item $\Def{}{c}{t}{T}/p\footnote{Opaque definitions are processed as assumptions.} ~=~ \Def{}{c}{t}{T}$
+ \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{p.c}{U}$
+ \item $\ModS{X}{S}/p ~=~ \ModA{X}{p.X}$
+ \item $\ModA{X}{p'}/p ~=~ \ModA{X}{p'}$
+ \item $\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$
+ \item $\Indpstr{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}{p} ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}$
+ \end{itemize}
+\item if $S\lra\functor{X}{S'}{S''}$ then $S/p=S$
+\end{itemize}
+The notation $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ denotes an
+inductive definition that is definitionally equal to the inductive
+definition in the module denoted by the path $p$. All rules which have
+$\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}$ as premises are also valid for
+$\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$. We give the formation rule
+for $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ below as well as
+the equality rules on inductive types and constructors. \\
+
+The module subtyping rules:
+\begin{description}
+\item[MSUB-STR]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WS{E;\elem_1;\dots;\elem_n}{\elem_{\sigma(i)}}{\elem'_i}
+ \textrm{ \ for } i=1..m \\
+ \sigma : \{1\dots m\} \ra \{1\dots n\} \textrm{ \ injective}
+ \end{array}
+ }{
+ \WS{E}{\struct{\elem_1;\dots;\elem_n}}{\struct{\elem'_1;\dots;\elem'_m}}
+ }
+}
+\item[MSUB-FUN]
+\inference{% T_1 -> T_2 <: T_1' -> T_2'
+ \frac{
+ \WS{E}{\overline{S_1'}}{\overline{S_1}}~~~~~~~~~~\WS{E;\ModS{X}{S_1'}}{\overline{S_2}}{\overline{S_2'}}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WS{E}{\functor{X}{S_1}{S_2}}{\functor{X}{S_1'}{S_2'}}
+ }
+}
+% these are derived rules
+% \item[MSUB-EQ]
+% \inference{%
+% \frac{
+% \WS{E}{T_1}{T_2}~~~~~~~~~~\WTERED{}{T_1}{=}{T_1'}~~~~~~~~~~\WTERED{}{T_2}{=}{T_2'}
+% }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \WS{E}{T_1'}{T_2'}
+% }
+% }
+% \item[MSUB-REFL]
+% \inference{%
+% \frac{
+% \WFT{E}{T}
+% }{
+% \WS{E}{T}{T}
+% }
+% }
+\end{description}
+Structure element subtyping rules:
+\begin{description}
+\item[ASSUM-ASSUM]
+\inference{%
+ \frac{
+ \WTELECONV{}{T_1}{T_2}
+ }{
+ \WSE{\Assum{}{c}{T_1}}{\Assum{}{c}{T_2}}
+ }
+}
+\item[DEF-ASSUM]
+\inference{%
+ \frac{
+ \WTELECONV{}{T_1}{T_2}
+ }{
+ \WSE{\Def{}{c}{t}{T_1}}{\Assum{}{c}{T_2}}
+ }
+}
+\item[ASSUM-DEF]
+\inference{%
+ \frac{
+ \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{c}{t_2}
+ }{
+ \WSE{\Assum{}{c}{T_1}}{\Def{}{c}{t_2}{T_2}}
+ }
+}
+\item[DEF-DEF]
+\inference{%
+ \frac{
+ \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
+ }{
+ \WSE{\Def{}{c}{t_1}{T_1}}{\Def{}{c}{t_2}{T_2}}
+ }
+}
+\item[IND-IND]
+\inference{%
+ \frac{
+ \WTECONV{}{\Gamma_P}{\Gamma_P'}%
+ ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
+ ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
+ }{
+ \WSE{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}%
+ {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
+ }
+}
+\item[INDP-IND]
+\inference{%
+ \frac{
+ \WTECONV{}{\Gamma_P}{\Gamma_P'}%
+ ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
+ ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
+ }{
+ \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
+ {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
+ }
+}
+\item[INDP-INDP]
+\inference{%
+ \frac{
+ \WTECONV{}{\Gamma_P}{\Gamma_P'}%
+ ~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
+ ~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
+ ~~~~~~\WTECONV{}{p}{p'}
+ }{
+ \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
+ {\Indp{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}{p'}}
+ }
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\item[MOD-MOD]
+\inference{%
+ \frac{
+ \WSE{S_1}{S_2}
+ }{
+ \WSE{\ModS{X}{S_1}}{\ModS{X}{S_2}}
+ }
+}
+\item[ALIAS-MOD]
+\inference{%
+ \frac{
+ \WTM{E}{p}{S_1}~~~~~~~~\WSE{S_1}{S_2}
+ }{
+ \WSE{\ModA{X}{p}}{\ModS{X}{S_2}}
+ }
+}
+\item[MOD-ALIAS]
+\inference{%
+ \frac{
+ \WTM{E}{p}{S_2}~~~~~~~~
+ \WSE{S_1}{S_2}~~~~~~~~\WTECONV{}{X}{p}
+ }{
+ \WSE{\ModS{X}{S_1}}{\ModA{X}{p}}
+ }
+}
+\item[ALIAS-ALIAS]
+\inference{%
+ \frac{
+ \WTECONV{}{p_1}{p_2}
+ }{
+ \WSE{\ModA{X}{p_1}}{\ModA{X}{p_2}}
+ }
+}
+\item[MODTYPE-MODTYPE]
+\inference{%
+ \frac{
+ \WSE{S_1}{S_2}~~~~~~~~\WSE{S_2}{S_1}
+ }{
+ \WSE{\ModType{Y}{S_1}}{\ModType{Y}{S_2}}
+ }
+}
+\end{description}
+New environment formation rules
+\begin{description}
+\item[WF-MOD]
+\inference{%
+ \frac{
+ \WF{E}{}~~~~~~~~\WFT{E}{S}
+ }{
+ \WF{E;\ModS{X}{S}}{}
+ }
+}
+\item[WF-MOD]
+\inference{%
+ \frac{
+\begin{array}{c}
+ \WS{E}{S_2}{S_1}\\
+ \WF{E}{}~~~~~\WFT{E}{S_1}~~~~~\WFT{E}{S_2}
+\end{array}
+ }{
+ \WF{E;\Mod{X}{S_1}{S_2}}{}
+ }
+}
+
+\item[WF-ALIAS]
+\inference{%
+ \frac{
+ \WF{E}{}~~~~~~~~~~~\WTE{}{p}{S}
+ }{
+ \WF{E,\ModA{X}{p}}{}
+ }
+}
+\item[WF-MODTYPE]
+\inference{%
+ \frac{
+ \WF{E}{}~~~~~~~~~~~\WFT{E}{S}
+ }{
+ \WF{E,\ModType{Y}{S}}{}
+ }
+}
+\item[WF-IND]
+\inference{%
+ \frac{
+ \begin{array}{c}
+ \WF{E;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}{}\\
+ \WT{E}{}{p:\struct{\elem_1;\dots;\elem_n;\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'};\dots}}\\
+ \WS{E}{\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}
+ \end{array}
+ }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
+ }
+}
+\end{description}
+Component access rules
+\begin{description}
+\item[ACC-TYPE]
+\inference{%
+ \frac{
+ \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Assum{}{c}{T};\dots}}
+ }{
+ \WTEG{p.c}{T}
+ }
+}
+\\
+\inference{%
+ \frac{
+ \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{T};\dots}}
+ }{
+ \WTEG{p.c}{T}
+ }
+}
+\item[ACC-DELTA]
+Notice that the following rule extends the delta rule defined in
+section~\ref{delta}
+\inference{%
+ \frac{
+ \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{U};\dots}}
+ }{
+ \WTEGRED{p.c}{\triangleright_\delta}{t}
+ }
+}
+\\
+In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
+ $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
+ $[c_1:C_1;\ldots;c_n:C_n]$
+\item[ACC-IND]
+\inference{%
+ \frac{
+ \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
+ }{
+ \WTEG{p.I_j}{(p_1:P_1)\ldots(p_r:P_r)A_j}
+ }
+}
+\inference{%
+ \frac{
+ \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
+ }{
+ \WTEG{p.c_m}{(p_1:P_1)\ldots(p_r:P_r){C_m}{I_j}{(I_j~p_1\ldots
+ p_r)}_{j=1\ldots k}}
+ }
+}
+\item[ACC-INDP]
+\inference{%
+ \frac{
+ \WT{E}{}{p}{\struct{\elem_1;\dots;\elem_i;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
+ }{
+ \WTRED{E}{}{p.I_i}{\triangleright_\delta}{p'.I_i}
+ }
+}
+\inference{%
+ \frac{
+ \WT{E}{}{p}{\struct{\elem_1;\dots;\elem_i;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
+ }{
+ \WTRED{E}{}{p.c_i}{\triangleright_\delta}{p'.c_i}
+ }
+}
+
+\end{description}
+
+% %%% replaced by \triangle_\delta
+% Module path equality is a transitive and reflexive closure of the
+% relation generated by ACC-MODEQ and ENV-MODEQ.
+% \begin{itemize}
+% \item []MP-EQ-REFL
+% \inference{%
+% \frac{
+% \WTEG{p}{T}
+% }{
+% \WTEG{p}{p}
+% }
+% }
+% \item []MP-EQ-TRANS
+% \inference{%
+% \frac{
+% \WTEGRED{p}{=}{p'}~~~~~~\WTEGRED{p'}{=}{p''}
+% }{
+% \WTEGRED{p'}{=}{p''}
+% }
+% }
+
+% \end{itemize}
+
+
+% $Id: RefMan-modr.tex 11197 2008-07-01 13:05:41Z soubiran $
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End:
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 21:58:47 +0000