From a20314166d9eca722e01dde21506c52dd8d8af74 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 23 Jan 2006 07:24:49 +0000 Subject: [PATCH] - use "sec:libmanagement" as label for compilation/decompilation (it was not uniformly used before) - typos in the disambiguation section --- helm/papers/matita/matita2.tex | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 49c531590..f1bc990c7 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -411,7 +411,7 @@ content level terms; presentation level terms. of preserving the coherence of the library and the database. For instance, when a notion is removed, all the notions that depend on it and their metadata are removed from the library. This aspect will be better detailed - in Sect.~\ref{decompilazione}. + in Sect.~\ref{sec:libmanagement}. \subsection{Partially specified terms} \emph{Partially specified terms} are CIC terms where subterms can be omitted. @@ -695,7 +695,7 @@ content selection and copy-paste. \subsection{Compilation and decompilation} -\label{compilazione} +\label{sec:libmanagement} The aim of this section is to describe the way matita preserves the consistency and the availability of the library @@ -912,7 +912,7 @@ translated (in multiple steps) to partially specified terms as sketched in Sect.~\ref{sec:contentintro}. The key component of the translation is the generic disambiguation algorithm -implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries} +implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries} and presented in~\cite{disambiguation}. In this section we present how to use such an algorithm in the context of the development of a library of formalized mathematics. We will see that using multiple passes of the algorithm, varying @@ -933,7 +933,7 @@ definition gt: nat \to nat \to Prop \def The \texttt{include} statement adds the requirement that the part of the library defining the notion of natural numbers should be defined before -processing the following definition. Note indeed that the algorithm presented +processing the what follows. Note indeed that the algorithm presented in~\cite{disambiguation} does not describe where interpretations for ambiguous expressions come from, since it is application-specific. As a first approximation, we will assume that in \MATITA{} they come from the library (i.e. @@ -1029,7 +1029,7 @@ theorem lt_to_Zlt_pos_pos: Unfortunately, none of the passes described above is able to disambiguate its type, no matter how aliases are defined. This is because the \OP{<} operator occurs twice in the content level term (it has two \emph{instances}) and two -different interpretation for it have to be used in order to obtain a refinable +different interpretations for it have to be used in order to obtain a refinable partially specified term. To address this issue, we have the ability to consider each instance of a single symbol as a different ambiguous expression in the content level term, and thus we can assign a different interpretation to each of @@ -1076,7 +1076,7 @@ the \texttt{pos} constructor itself), the theorem can be disambiguated using twice that coercion on the left hand side of the implication. The obtained partially specified term however would not probably be the expected one, being a theorem which prove a trivial implication. For this reason we choose to always -prefer fresh instances over implicit coercion, i.e. we always attempt +prefer fresh instances over implicit coercions, i.e. we always attempt disambiguation passes with fresh instances before attempting passes with implicit coercions. -- 2.39.2