uniformly used before)
- typos in the disambiguation section
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
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.
\subsection{Partially specified terms}
\emph{Partially specified terms} are CIC terms where subterms can be omitted.
\subsection{Compilation and decompilation}
\subsection{Compilation and decompilation}
+\label{sec:libmanagement}
The aim of this section is to describe the way matita
preserves the consistency and the availability of the library
The aim of this section is to describe the way matita
preserves the consistency and the availability of the library
Sect.~\ref{sec:contentintro}.
The key component of the translation is the generic disambiguation algorithm
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
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
The \texttt{include} statement adds the requirement that the part of the library
defining the notion of natural numbers should be defined before
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.
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.
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
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
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
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
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.
disambiguation passes with fresh instances before attempting passes with
implicit coercions.