From 86bbddfd3dd3c89a582f47d2f42d5d33686dfe53 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Tue, 5 Mar 2024 10:14:47 -0600
Subject: [PATCH] Clarify omitting :args in anchor
---
spec/changelog.tex | 6 ++++++
spec/doc.tex | 9 +++++++--
2 files changed, 13 insertions(+), 2 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index 8fea177..79db837 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -5,6 +5,12 @@ Breaking changes:
\item Allow arbitrary extra annotations in \texttt{assume} commands.
\end{itemize}
+Clarifications:
+\begin{itemize}
+ \item Clarify that the \texttt{:args} annotation in \texttt{anchor} can be
+ omitted if the list is empty.
+\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 f68c66c..49e333b 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -820,9 +820,14 @@ pushes precisely $c_1,\dots, c_n$ onto the context.
Since contexts can only be manipulated by push and pop, context manipulations
are nested. The \inlineAlethe{anchor} commands push onto the context and the
corresponding \inlineAlethe{step} commands pop from the context.
+%
To indicate these changes to the context, every anchor is associated with a list
-of fixed variables and mappings.
-This list can be empty.
+of fixed variables and mappings. The list is provided by the \inlineAlethe{:args}
+annotation. If the list is empty, the \inlineAlethe{:args} annotation is
+omitted\footnote{The only rule that allows an empty list is the
+\proofRule{subproof} rule. Since this rule corresponds to implication introduction,
+it does not interact with binders.}.
+%
Note that, when an \inlineAlethe{anchor} command extends a context $\Gamma$ with
some mappings $x_1 \mapsto t_1, \dots, x_n \mapsto t_n$,
then the terms $t_i$ are normalized by applying
--
GitLab