From 1e2d180b73572a4bc4be1d502d3014696ed6e2b4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 19 Nov 2015 16:18:51 +0100
Subject: [PATCH] COFE on type with leibniz equality.
---
iris/cofe.v | 2 ++
prelude/base.v | 2 ++
2 files changed, 4 insertions(+)
diff --git a/iris/cofe.v b/iris/cofe.v
index eb43c721c..7c48363ad 100644
--- a/iris/cofe.v
+++ b/iris/cofe.v
@@ -272,6 +272,8 @@ Section discrete_cofe.
End discrete_cofe.
Arguments discrete_cofeC _ {_ _}.
+Definition leibniz_cofeC (A : Type) : cofeT := @discrete_cofeC A equivL _.
+
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
Arguments Later {_} _.
diff --git a/prelude/base.v b/prelude/base.v
index 497e040cf..30ec94664 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -194,6 +194,8 @@ Ltac unfold_leibniz := repeat
setoid_rewrite <-(leibniz_equiv (A:=A))
end.
+Definition equivL {A} : Equiv A := (=).
+
(** A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
instances for all operational type classes in this development. *)
--
GitLab