From 6010b7c4b3d27cf8624266077f5725cfc06eca04 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 10 Dec 2018 12:24:51 +0100
Subject: [PATCH] A comment that `agree_car` is not non-expansive.
---
theories/algebra/agree.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 355f976b3..ad8dc5a55 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -26,6 +26,9 @@ Proof.
Thus Ag(T) is not necessarily complete.
*)
+(** Note that the projection [agree_car] is not non-expansive, so it cannot be
+used in the logic. If you need to get a witness out, you should use the
+lemma [to_agree_uninjN] instead. *)
Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
--
GitLab