Skip to content

Commit

Permalink
small corrections (#171)
Browse files Browse the repository at this point in the history
  • Loading branch information
Casteran authored Jan 8, 2024
1 parent c27a80b commit b5753c3
Show file tree
Hide file tree
Showing 3 changed files with 159 additions and 167 deletions.
7 changes: 5 additions & 2 deletions doc/chapter-primrec.tex
Original file line number Diff line number Diff line change
Expand Up @@ -879,15 +879,18 @@ \subsection{Looking for a contradiction}
Thus, our impossibility proof is just a sequence of easy small steps.

\begin{remark}
In the following snippet, \emph{Alectryon}'s \texttt{Latex} generator prints the \emph{local definition} of $x$ (as the maximum of $2$ and $m$) as a simple \emph{declaration} \texttt{x: nat}.
In the following snippet, some versions \emph{Alectryon}'s \texttt{Latex} generator print the \emph{local definition} of $x$ (as the maximum of $2$ and $m$) as a simple \emph{declaration} \texttt{x: nat}.
Thus the proof script is correct, but the three last sub-goals are not correctly displayed, since
they do not show how the inequalities $2\leq x$ and $m \leq x$ could be inferred by \texttt{lia}.

A correct goal display can be obtained with
\href{https://github.com/Casteran/alectryonFix}{this fork}.
\end{remark}

\input{movies/snippets/AckNotPR/AckNotPR}

\begin{remark}
It is easy to prove that any unary function which dominates \texttt{fun n => Ack n n} fails to be primitive recursive. To this end, we use an instance of \texttt{majorAnyPR} dealing with unary functions.
It is easy to prove that any unary function which dominates (\texttt{fun n => Ack n n}) fails to be primitive recursive. To this end, we use an instance of \texttt{majorAnyPR} dealing with unary functions.

\vspace{4pt}
\noindent
Expand Down
Loading

0 comments on commit b5753c3

Please sign in to comment.