From a4fc20bc7d94bfcaa1d3edfa5259349f80cc25a9 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 16 Apr 2019 00:59:27 +0200
Subject: [PATCH] Documentation for #237
That's the documentation I'd have wanted to see, and viceversa the lack of this
rule implied (to me) that this wouldn't work.
---
docs/ghost-state.tex | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 8d1514140..2d259b3d3 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -60,7 +60,13 @@ It turns out that we can somewhat mitigate this trouble by working below the fol
This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
-In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless propositions.
+In other words, when working below the except-0 modality, we can \emph{strip
+ away} the later from timeless propositions. In fact, we can strip away later
+from timeless propositions even when working under the later modality:
+\begin{mathpar}
+ \infer{\prop \proves \later \propB}
+ {\later\prop \proves \later\propB}
+\end{mathpar}
The following rules can be derived about except-0:
\begin{mathpar}
--
GitLab