From c02adf583d7e1432f4fafa55c8c2e27238698a90 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 17 Apr 2019 17:57:30 +0200
Subject: [PATCH] Explain why the rule looks different
---
docs/ghost-state.tex | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index cdf29ac09..224999e23 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -67,6 +67,12 @@ from timeless propositions even when working under the later modality:
\infer{\timeless{\prop} \and \prop \proves \later \propB}
{\later\prop \proves \later\propB}
\end{mathpar}
+This rule looks different from the above ones, because we still do not have that
+\begin{mathpar}
+ \inferH{later-fake-rule}{\timeless{\prop}}
+ {\later\prop \proves \prop}
+\end{mathpar}
+
The following rules can be derived about except-0:
\begin{mathpar}
--
GitLab