From ed34db952cec04a7e4c38474501414562797eef8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 13 Jan 2020 20:30:49 +0100
Subject: [PATCH] Add some documentation.

---
 theories/si_logic/bi.v     | 3 +++
 theories/si_logic/siprop.v | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index 7280b9afe..2efd1b8bf 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -5,6 +5,9 @@ Import siProp_primitive.
 (** BI instances for [siProp], and re-stating the remaining primitive laws in
 terms of the BI interface.  This file does *not* unseal. *)
 
+(** We pick [*] and [-*] to coincide with [∧] and [→], respectively. This seems
+to be the most reasonable choice to fit a "pure" higher-order logic into the
+proofmode's BI framework. *)
 Definition siProp_emp : siProp := siProp_pure True.
 Definition siProp_sep : siProp → siProp → siProp := siProp_and.
 Definition siProp_wand : siProp → siProp → siProp := siProp_impl.
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index d265fe417..5619e0574 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -1,6 +1,9 @@
 From iris.algebra Require Export ofe.
 From iris.bi Require Import notation.
 
+(** The type [siProp] defines "plain" step-indexed propositions, on which we
+define the usual connectives of higher-order logic, and prove that these satisfy
+the usual laws of higher-order logic. *)
 Record siProp := SiProp {
   siProp_holds :> nat → Prop;
   siProp_closed n1 n2 : siProp_holds n1 → n2 ≤ n1 → siProp_holds n2
-- 
GitLab