From e935525c11be10b17aaab193dde56c373b709c2a Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Tue, 30 Jan 2024 17:18:31 -0600
Subject: [PATCH] Fix typos in example
---
spec/changelog.tex | 2 +-
spec/doc.tex | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index 0e0dc1b..8fea177 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -1,6 +1,6 @@
\subsection*{Unreleased}
-Braking changes:
+Breaking changes:
\begin{itemize}
\item Allow arbitrary extra annotations in \texttt{assume} commands.
\end{itemize}
diff --git a/spec/doc.tex b/spec/doc.tex
index 2ce54c6..a50de4a 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -858,12 +858,12 @@ expressed as a concrete proof.
\begin{AletheVerb}
(assume h1 (forall ((x S)) (P x)))
(assume h2 (not (forall ((y S)) (P y))))
-(anchor :step t5 :args ((:= x y)))
+(anchor :step t5 :args ((y S) (:= x y)))
(step t3 (cl (= x y)) :rule refl)
(step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
:rule bind)
-(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
+(step t6 (cl (not (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
(not (forall ((x S)) (P x)))
(forall ((y S)) (P y))) :rule equiv_pos2)
(step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
--
GitLab