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.tex586
1 files changed, 0 insertions, 586 deletions
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
deleted file mode 100644
index a52c1847..00000000
--- a/doc/refman/RefMan-modr.tex
+++ /dev/null
@@ -1,586 +0,0 @@
-\chapter{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 \Impl\ and is either a
-definition of a constant, an assumption, a definition of an inductive
-or a definition of a module or a module type abbreviation.
-
-\paragraph{Module expression.} It is denoted by $M$ and can be:
-\begin{itemize}
-\item an access path $p$
-\item a structure $\struct{\nelist{\Impl}{;}}$
-\item a functor $\functor{X}{T}{M'}$, where $X$ is a module variable,
- $T$ is a module type and $M'$ is a module expression
-\item an application of access paths $p' p''$
-\end{itemize}
-
-\paragraph{Signature element.} It is denoted by \Spec, it is a
-specification of a constant, an assumption, an inductive, a module or
-a module type abbreviation.
-
-\paragraph{Module type,} denoted by $T$ can be:
-\begin{itemize}
-\item a module type name
-\item an access path $p$
-\item a signature $\sig{\nelist{\Spec}{;}}$
-\item a functor type $\funsig{X}{T'}{T''}$, where $T'$ and $T''$ are
- module types
-\end{itemize}
-
-\paragraph{Module definition,} written $\Mod{X}{T}{M}$ can be a
-structure element. It consists of a module variable $X$, a module type
-$T$ and a module expression $M$.
-
-\paragraph{Module specification,} written $\ModS{X}{T}$ or
-$\ModSEq{X}{T}{p}$ can be a signature element or a part of an
-environment. It consists of a module variable $X$, a module type $T$
-and, optionally, a module path $p$.
-
-\paragraph{Module type abbreviation,} written $\ModType{S}{T}$, where
-$S$ is a module type name and $T$ is a module type.
-
-
-\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 signature elements.
-Terms, apart from variables, constants and complex terms,
-include also access paths.
-
-We also need additional typing judgments:
-\begin{itemize}
-\item \WFT{E}{T}, denoting that a module type $T$ is well-formed,
-
-\item \WTM{E}{M}{T}, denoting that a module expression $M$ has type $T$ in
-environment $E$.
-
-\item \WTM{E}{\Impl}{\Spec}, denoting that an implementation $\Impl$
- verifies a specification $\Spec$
-
-\item \WS{E}{T_1}{T_2}, denoting that a module type $T_1$ is a subtype of a
-module type $T_2$.
-
-\item \WS{E}{\Spec_1}{\Spec_2}, denoting that a specification
- $\Spec_1$ is more precise that a specification $\Spec_2$.
-\end{itemize}
-The rules for forming module types are the following:
-\begin{description}
-\item[WF-SIG]
-\inference{%
- \frac{
- \WF{E;E'}{}
- }{%%%%%%%%%%%%%%%%%%%%%
- \WFT{E}{\sig{E'}}
- }
-}
-\item[WF-FUN]
-\inference{%
- \frac{
- \WFT{E;\ModS{X}{T}}{T'}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WFT{E}{\funsig{X}{T}{T'}}
- }
-}
-\end{description}
-Rules for typing module expressions:
-\begin{description}
-\item[MT-STRUCT]
-\inference{%
- \frac{
- \begin{array}{c}
- \WFT{E}{\sig{\Spec_1;\dots;\Spec_n}}\\
- \WTM{E;\Spec_1;\dots;\Spec_{i-1}}{\Impl_i}{\Spec_i}
- \textrm{ \ \ for } i=1\dots n
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WTM{E}{\struct{\Impl_1;\dots;\Impl_n}}{\sig{\Spec_1;\dots;\Spec_n}}
- }
-}
-\item[MT-FUN]
-\inference{%
- \frac{
- \WTM{E;\ModS{X}{T}}{M}{T'}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WTM{E}{\functor{X}{T}{M}}{\funsig{X}{T}{T'}}
- }
-}
-\item[MT-APP]
-\inference{%
- \frac{
- \begin{array}{c}
- \WTM{E}{p}{\funsig{X_1}{T_1}{\!\dots\funsig{X_n}{T_n}{T'}}}\\
- \WTM{E}{p_i}{T_i\{X_1/p_1\dots X_{i-1}/p_{i-1}\}}
- \textrm{ \ \ for } i=1\dots n
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WTM{E}{p\; p_1 \dots p_n}{T'\{X_1/p_1\dots X_n/p_n\}}
- }
-}
-\item[MT-SUB]
-\inference{%
- \frac{
- \WTM{E}{M}{T}~~~~~~~~~~~~\WS{E}{T}{T'}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WTM{E}{M}{T'}
- }
-}
-\item[MT-STR]
-\inference{%
- \frac{
- \WTM{E}{p}{T}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WTM{E}{p}{T/p}
- }
-}
-\end{description}
-The last rule, called strengthening is used to make all module fields
-manifestly equal to themselves. The notation $T/p$ has the following
-meaning:
-\begin{itemize}
-\item if $T=\sig{\Spec_1;\dots;\Spec_n}$ then
- $T/p=\sig{\Spec_1/p;\dots;\Spec_n/p}$ where $\Spec/p$ is defined as
- follows:
- \begin{itemize}
- \item $\Def{}{c}{U}{t}/p ~=~ \Def{}{c}{U}{t}$
- \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{p.c}{U}$
- \item $\ModS{X}{T}/p ~=~ \ModSEq{X}{T/p.X}{p.X}$
- \item $\ModSEq{X}{T}{p'}/p ~=~ \ModSEq{X}{T/p}{p'}$
- \item $\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$
- \item $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}$
- \end{itemize}
-\item if $T=\funsig{X}{T'}{T''}$ then $T/p=T$
-\item if $T$ is an access path or a module type name, then we have to
- unfold its definition and proceed according to the rules above.
-\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-SIG]
-\inference{%
- \frac{
- \begin{array}{c}
- \WS{E;\Spec_1;\dots;\Spec_n}{\Spec_{\sigma(i)}}{\Spec'_i}
- \textrm{ \ for } i=1..m \\
- \sigma : \{1\dots m\} \ra \{1\dots n\} \textrm{ \ injective}
- \end{array}
- }{
- \WS{E}{\sig{\Spec_1;\dots;\Spec_n}}{\sig{\Spec'_1;\dots;\Spec'_m}}
- }
-}
-\item[MSUB-FUN]
-\inference{% T_1 -> T_2 <: T_1' -> T_2'
- \frac{
- \WS{E}{T_1'}{T_1}~~~~~~~~~~\WS{E;\ModS{X}{T_1'}}{T_2}{T_2'}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WS{E}{\funsig{X}{T_1}{T_2}}{\funsig{X}{T_1'}{T_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}
-Specification subtyping rules:
-\begin{description}
-\item[ASSUM-ASSUM]
-\inference{%
- \frac{
- \WTELECONV{}{U_1}{U_2}
- }{
- \WSE{\Assum{}{c}{U_1}}{\Assum{}{c}{U_2}}
- }
-}
-\item[DEF-ASSUM]
-\inference{%
- \frac{
- \WTELECONV{}{U_1}{U_2}
- }{
- \WSE{\Def{}{c}{t}{U_1}}{\Assum{}{c}{U_2}}
- }
-}
-\item[ASSUM-DEF]
-\inference{%
- \frac{
- \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{c}{t_2}
- }{
- \WSE{\Assum{}{c}{U_1}}{\Def{}{c}{t_2}{U_2}}
- }
-}
-\item[DEF-DEF]
-\inference{%
- \frac{
- \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
- }{
- \WSE{\Def{}{c}{t_1}{U_1}}{\Def{}{c}{t_2}{U_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[MODS-MODS]
-\inference{%
- \frac{
- \WSE{T_1}{T_2}
- }{
- \WSE{\ModS{m}{T_1}}{\ModS{m}{T_2}}
- }
-}
-\item[MODEQ-MODS]
-\inference{%
- \frac{
- \WSE{T_1}{T_2}
- }{
- \WSE{\ModSEq{m}{T_1}{p}}{\ModS{m}{T_2}}
- }
-}
-\item[MODS-MODEQ]
-\inference{%
- \frac{
- \WSE{T_1}{T_2}~~~~~~~~\WTECONV{}{m}{p_2}
- }{
- \WSE{\ModS{m}{T_1}}{\ModSEq{m}{T_2}{p_2}}
- }
-}
-\item[MODEQ-MODEQ]
-\inference{%
- \frac{
- \WSE{T_1}{T_2}~~~~~~~~\WTECONV{}{p_1}{p_2}
- }{
- \WSE{\ModSEq{m}{T_1}{p_1}}{\ModSEq{m}{T_2}{p_2}}
- }
-}
-\item[MODTYPE-MODTYPE]
-\inference{%
- \frac{
- \WSE{T_1}{T_2}~~~~~~~~\WSE{T_2}{T_1}
- }{
- \WSE{\ModType{S}{T_1}}{\ModType{S}{T_2}}
- }
-}
-\end{description}
-Verification of the specification
-\begin{description}
-\item[IMPL-SPEC]
-\inference{%
- \frac{
- \begin{array}{c}
- \WF{E;\Spec}{}\\
- \Spec \textrm{\ is one of } {\sf Def, Assum, Ind, ModType}
- \end{array}
- }{
- \WTE{}{\Spec}{\Spec}
- }
-}
-\item[MOD-MODS]
-\inference{%
- \frac{
- \WF{E;\ModS{m}{T}}{}~~~~~~~~\WTE{}{M}{T}
- }{
- \WTE{}{\Mod{m}{T}{M}}{\ModS{m}{T}}
- }
-}
-\item[MOD-MODEQ]
-\inference{%
- \frac{
- \WF{E;\ModSEq{m}{T}{p}}{}~~~~~~~~~~~\WTECONV{}{p}{p'}
- }{
- \WTE{}{\Mod{m}{T}{p'}}{\ModSEq{m}{T}{p'}}
- }
-}
-\end{description}
-New environment formation rules
-\begin{description}
-\item[WF-MODS]
-\inference{%
- \frac{
- \WF{E}{}~~~~~~~~\WFT{E}{T}
- }{
- \WF{E;\ModS{m}{T}}{}
- }
-}
-\item[WF-MODEQ]
-\inference{%
- \frac{
- \WF{E}{}~~~~~~~~~~~\WTE{}{p}{T}
- }{
- \WF{E,\ModSEq{m}{T}{p}}{}
- }
-}
-\item[WF-MODTYPE]
-\inference{%
- \frac{
- \WF{E}{}~~~~~~~~~~~\WFT{E}{T}
- }{
- \WF{E,\ModType{S}{T}}{}
- }
-}
-\item[WF-IND]
-\inference{%
- \frac{
- \begin{array}{c}
- \WF{E;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}{}\\
- \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'};\dots}}\\
- \WS{E}{\subst{\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}{p.l}{l}_{l
- \in \lab{Spec_1;\dots;Spec_n}}}{\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}{\sig{\Spec_1;\dots;Spec_i;\Assum{}{c}{U};\dots}}
- }{
- \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\\
-\inference{%
- \frac{
- \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{t}{U};\dots}}
- }{
- \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\item[ACC-DELTA]
-Notice that the following rule extends the delta rule defined in
-section~\ref{delta}
-\inference{%
- \frac{
- \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{t}{U};\dots}}
- }{
- \WTEGRED{p.c}{\triangleright_\delta}{\subst{t}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\\
-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}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
- }{
- \WTEG{p.I_j}{\subst{(p_1:P_1)\ldots(p_r:P_r)A_j}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\inference{%
- \frac{
- \WTEG{p}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
- }{
- \WTEG{p.c_m}{\subst{(p_1:P_1)\ldots(p_r:P_r)\subst{C_m}{I_j}{(I_j~p_1\ldots
- p_r)}_{j=1\ldots k}}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\item[ACC-INDP]
-\inference{%
- \frac{
- \WT{E}{}{p}{\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
- }{
- \WTRED{E}{}{p.I_i}{\triangleright_\delta}{p'.I_i}
- }
-}
-\inference{%
- \frac{
- \WT{E}{}{p}{\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
- }{
- \WTRED{E}{}{p.c_i}{\triangleright_\delta}{p'.c_i}
- }
-}
-%%%%%%%%%%%%%%%%%%%%%%%%%%% MODULES
-\item[ACC-MOD]
-\inference{%
- \frac{
- \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModS{m}{T};\dots}}
- }{
- \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\\
-\inference{%
- \frac{
- \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModSEq{m}{T}{p'};\dots}}
- }{
- \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\item[ACC-MODEQ]
-\inference{%
- \frac{
- \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModSEq{m}{T}{p'};\dots}}
- }{
- \WTEGRED{p.m}{\triangleright_\delta}{\subst{p'}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\item[ACC-MODTYPE]
-\inference{%
- \frac{
- \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModType{S}{T};\dots}}
- }{
- \WTEGRED{p.S}{\triangleright_\delta}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
- }
-}
-\end{description}
-The function $\lab{}$ is used to calculate the set of label of
-the set of specifications. It is defined by
-$\lab{\Spec_1;\dots;\Spec_n}=\lab{\Spec_1}\cup\dots;\cup\lab{\Spec_n}$
-where $\lab{\Spec}$ is defined as follows:
-\begin{itemize}
-\item $\lab{\Assum{\Gamma}{c}{U}}=\{c\}$,
-\item $\lab{\Def{\Gamma}{c}{t}{U}}=\{c\}$,
-\item
- $\lab{\Ind{\Gamma}{\Gamma_P}{\Gamma_C}{\Gamma_I}}=\dom{\Gamma_C}\cup\dom{\Gamma_I}$,
-\item $\lab{\ModS{m}{T}}=\{m\}$,
-\item $\lab{\ModSEq{m}{T}{M}}=\{m\}$,
-\item $\lab{\ModType{S}{T}}=\{S\}$
-\end{itemize}
-Environment access for modules and module types
-\begin{description}
-\item[ENV-MOD]
-\inference{%
- \frac{
- \WF{E;\ModS{m}{T};E'}{\Gamma}
- }{
- \WT{E;\ModS{m}{T};E'}{\Gamma}{m}{T}
- }
-}
-\item[]
-\inference{%
- \frac{
- \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
- }{
- \WT{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{T}
- }
-}
-\item[ENV-MODEQ]
-\inference{%
- \frac{
- \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
- }{
- \WTRED{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{\triangleright_\delta}{p}
- }
-}
-\item[ENV-MODTYPE]
-\inference{%
- \frac{
- \WF{E;\ModType{S}{T};E'}{\Gamma}
- }{
- \WTRED{E;\ModType{S}{T};E'}{\Gamma}{S}{\triangleright_\delta}{T}
- }
-}
-\item[ENV-INDP]
-\inference{%
- \frac{
- \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
- }{
- \WTRED{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}{I_i}{\triangleright_\delta}{p.I_i}
- }
-}
-\inference{%
- \frac{
- \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
- }{
- \WTRED{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{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 8606 2006-02-23 13:58:10Z herbelin $
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End:
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 09:47:20 +0000