From 5628ac5516269caf5429f15ac3a3351f58fe2a18 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 May 2020 13:17:42 +0200
Subject: [PATCH] Comment for `internal_eq` file.

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

diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 62ce1bfd5..6e97b92e6 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -1,6 +1,10 @@
 From iris.bi Require Import derived_laws_sbi big_op.
 Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
+(** This file defines a type class for BIs with a notion of internal equality.
+Internal equality is not part of the [bi] canonical structure as [internal_eq]
+can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
+[▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
 Class InternalEq (PROP : bi) :=
   internal_eq : ∀ {A : ofeT}, A → A → PROP.
 Arguments internal_eq {_ _ _} _ _ : simpl never.
-- 
GitLab