From f30188af9d3846512c2d89260f9474358a333be0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 12 Feb 2018 17:12:56 +0100
Subject: [PATCH] document the RA model briefly

---
 theories/bi/interface.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 990145281..cf3780875 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -42,6 +42,16 @@ Section bi_mixin.
   Local Notation "x ≡ y" := (sbi_internal_eq _ x y).
   Local Notation "â–· P" := (sbi_later P).
 
+  (** * Axioms for a general BI (logic of bunched implications) *)
+
+  (** The following axioms are satisifed by both affine and linear BIs, and BIs
+  that combine both kinds of resources. In particular, we have an "ordered RA"
+  model satisfying all these axioms. For this model, we extend RAs with an
+  arbitrary partial order, and up-close resources wrt. that order (instead of
+  extension order).  We demand composition to be monotone wrt. the order.  We
+  define [emp := λ r, ε ≼ r]; persisently is still defined with the core: [□ P
+  := λ r, P (core r)].  *)
+
   Record BiMixin := {
     bi_mixin_entails_po : PreOrder bi_entails;
     bi_mixin_equiv_spec P Q : equiv P Q ↔ (P ⊢ Q) ∧ (Q ⊢ P);
-- 
GitLab