From 8ba8502ddb3f809bfcc5b43eaf67658c5c089ef1 Mon Sep 17 00:00:00 2001
From: Eugene Flesselle <eugene@flesselle.net>
Date: Fri, 24 Nov 2023 10:37:54 +0100
Subject: [PATCH] Fix small typos
---
Reference Manual/kernel.tex | 6 +++---
Reference Manual/quickguide.tex | 2 +-
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/Reference Manual/kernel.tex b/Reference Manual/kernel.tex
index 8d0fd362..1f55e586 100644
--- a/Reference Manual/kernel.tex
+++ b/Reference Manual/kernel.tex
@@ -165,7 +165,7 @@ For formulas, we use greek letters such as $\phi$, $\psi$, $\tau$ to denote arbi
\subsection{Substitution}
\label{subsec:substitution}
-On top of basic building blocks of terms and formulas, there is one important type of operations: substitution of schematic symbols, which has to be implemented in a capture-avoiding way. We start with the subcase of variable substitution:
+On top of basic building blocks of terms and formulas, there is one important type of operation: substitution of schematic symbols, which has to be implemented in a capture-avoiding way. We start with the subcase of variable substitution:
\begin{definition}[Capture-avoiding Substitution of variables]
Given a base term $t$, a variable $x$ and another term $r$, the substitution of $x$ by $r$ inside $t$ is denoted by $ t[x := r] $ and is computed by replacing all occurences of $x$ by $r$.
@@ -752,7 +752,7 @@ LISA's kernel allows to define two kinds of objects: Function (or Term) symbols
FunctionDefinition(f, y, lambda(Seq(x1,...,x2), φ))
\end{lstlisting}
corresponds to \\
- \hspace*{1.3em}``For any $\vec{x}$, let $f^n(\vec{x}) \textnormal{ be the unique } y \textnormal{ such that } \phi$ holds."
+ \hspace*{1.3em}``For any $\vec{x}$, let $f^n(\vec{x}) \textnormal{ be the unique } y \textnormal{ such that } \varphi$ holds."
\caption{Definitions in LISA.}
\label{fig:definitions}
@@ -1078,7 +1078,7 @@ Now, consider again
val f: SchematicFunctionLabel("f", 2)
\end{lstlisting}
even with the above \lstinline|apply| trick, \lstinline|f(x, y)| would not compile, since \lstinline|f| can apply to \lstinline|Term| arguments, but not to \lstinline|TermLabel|. Hence we first need to apply \lstinline|x| and \lstinline|y| to an empty list of argument, such as in \lstinline|f(x(), y())|.
-This can be done automatically with implicit conversions. Implicit conversion is the mechanism allowing to cast an object of a type to an other in a canonical way. It is define with the \lstinline|given| keyword:
+This can be done automatically with implicit conversions. Implicit conversion is the mechanism allowing to cast an object of a type to an other in a canonical way. It is defined with the \lstinline|given| keyword:
%
\begin{lstlisting}[language=Scala]
given Conversion[TermLabel, Term] = (t: Term) => Term(t, Seq())
diff --git a/Reference Manual/quickguide.tex b/Reference Manual/quickguide.tex
index 0b39e7d5..97545b6d 100644
--- a/Reference Manual/quickguide.tex
+++ b/Reference Manual/quickguide.tex
@@ -186,7 +186,7 @@ is equivalent to
have (Y) by Tactic2(s1)
\end{lstlisting}
\end{minipage}
-\lstinline|thenHave| allows us to not give a name to every step when we're doing linear reasoning. Finally, in lines 5 and 8, we see that tactic can refer not only to steps of the current proof, but also to previously proven theorems and axioms, such as \lstinline|emptySetAxiom|. The \lstinline|of| keyword indicates the the axiom (or step) is instantiated in a particular way. For example:
+\lstinline|thenHave| allows us to not give a name to every step when we're doing linear reasoning. Finally, in lines 5 and 8, we see that tactic can refer not only to steps of the current proof, but also to previously proven theorems and axioms, such as \lstinline|emptySetAxiom|. The \lstinline|of| keyword indicates the axiom (or step) is instantiated in a particular way. For example:
\noindent\begin{minipage}{\linewidth}\vspace{1em}
\begin{lstlisting}[language=lisa, frame=single]
emptySetAxiom // == !(x ∈ ∅)
--
GitLab