From 98ddbead4f5e5a3a90c26469182923ea19cb3a43 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 Oct 2018 12:52:11 +0100
Subject: [PATCH] Document `state_interp` and `fork_post`.

---
 theories/program_logic/weakestpre.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 4d71c1a4b..3209c4e5d 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -7,7 +7,17 @@ Import uPred.
 
 Class irisG' (Λstate Λobservation : Type) (Σ : gFunctors) := IrisG {
   iris_invG :> invG Σ;
+
+  (** The state interpretation is an invariant that should hold in between each
+  step of reduction. Here [Λstate] is the global state, [list Λobservation] are
+  the remaining observations, and [nat] is the number of forked-off threads
+  (not the total number of threads, which is one higher because there is always
+  a main thread). *)
   state_interp : Λstate → list Λobservation → nat → iProp Σ;
+
+  (** A fixed postcondition for any forked-off thread. For most languages, e.g.
+  heap_lang, this will simply be [True]. However, it is useful if one wants to
+  keep track of resources precisely, as in e.g. Iron. *)
   fork_post : iProp Σ;
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) (observation Λ) Σ).
-- 
GitLab