From 3673d5fd60c5606ed68108416ba3978258684f8c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 17 Jun 2018 19:34:42 +0200
Subject: [PATCH] comment for how we plan to generalize the WP notation if
 necessary

---
 theories/bi/weakestpre.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index 212476324..d09068871 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -23,7 +23,10 @@ thread IDs (as in iGPS).
 
 For the case of stuckness bits, there are two specific notations
 [WP e @ E {{ Φ }}] and [WP e @ E ?{{ Φ }}], which forces [A] to be [stuckness],
-and [s] to be [NotStuck] or [MaybeStuck]. *)
+and [s] to be [NotStuck] or [MaybeStuck].  This will fail to typecheck if [A] is
+not [stuckness].  If we ever want to use the notation [WP e @ E {{ Φ }}] with a
+different [A], the plan is to generalize the notation to use [Inhabited] instead
+to pick a default value depending on [A]. *)
 Class Wp (Λ : language) (PROP A : Type) :=
   wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
 Arguments wp {_ _ _ _} _ _ _%E _%I.
-- 
GitLab