From bfb354c83857f872976feb25969809d80e421f17 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Thu, 21 Dec 2023 09:53:33 -0600
Subject: [PATCH] Allow extra annotations
---
spec/changelog.tex | 7 +++++++
spec/doc.tex | 2 +-
2 files changed, 8 insertions(+), 1 deletion(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index a058885..0e0dc1b 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -1,3 +1,10 @@
+\subsection*{Unreleased}
+
+Braking changes:
+\begin{itemize}
+ \item Allow arbitrary extra annotations in \texttt{assume} commands.
+\end{itemize}
+
\subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}}
This release overhauls the entire document, but introduces only few
diff --git a/spec/doc.tex b/spec/doc.tex
index cea62c5..2ce54c6 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -691,7 +691,7 @@ An Alethe proof is a list of commands.
\[
\begin{array}{r c l}
\grNT{proof} &\grRule & \grNT{proof\_command}^{*} \\
- \grNT{proof\_command} &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\
+ \grNT{proof\_command} &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
&\grOr & \textAlethe{(step}\; \grNT{symbol}\; \grNT{clause}
\; \textAlethe{:rule}\; \grNT{symbol} \\
& & \quad \grNT{premises\_annotation}^{?} \\
--
GitLab