From 3cb126caa909f0d7a5d250f324772dbe2be7e513 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 2 Sep 2017 21:55:52 +0200
Subject: [PATCH] More documentation for the type class logical operators.

---
 theories/base.v | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 9721f053..c0d9b428 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -25,9 +25,22 @@ Arguments unseal {_ _} _.
 Arguments seal_eq {_ _} _.
 Unset Primitive Projections.
 
-(* The [Or] class is useful for efficiency: instead of having two instances
-[P → Q1 → R] and [P → Q2 → R] we could have one instance [P → Or Q1 Q2 → R],
-which avoids the need to derive [P] twice. *)
+(* Below we define type class versions of the common logical operators. It is
+important to note that we duplicate the definitions, and do not declare the
+existing logical operators as type classes. That is, we do not say:
+
+  Existing Class or.
+  Existing Class and.
+
+If we could define the existing logical operators as classes, there is no way
+of disambiguating whether a premise of a lemma should be solved by type class
+resolution or not.
+
+These classes are useful for two purposes: writing complicated type class
+premises in a more concise way, and for efficiency. For example, using the [Or]
+class, instead of defining two instances [P → Q1 → R] and [P → Q2 → R] we could
+have one instance [P → Or Q1 Q2 → R]. When we declare the instance that way, we
+avoid the need to derive [P] twice. *)
 Inductive TCOr (P1 P2 : Prop) : Prop :=
   | TCOr_l : P1 → TCOr P1 P2
   | TCOr_r : P2 → TCOr P1 P2.
-- 
GitLab