From 20bc8ab53a8a2777e54dea261b906106e7daf373 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Jun 2016 16:14:43 -0700 Subject: Add Unit.v --- src/Util/Unit.v | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 src/Util/Unit.v (limited to 'src/Util/Unit.v') diff --git a/src/Util/Unit.v b/src/Util/Unit.v new file mode 100644 index 000000000..cf5c4f669 --- /dev/null +++ b/src/Util/Unit.v @@ -0,0 +1,8 @@ +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. + +(* an equivalence for a relation on trivial things, like [unit] *) +Global Instance Equivalence_trivial {A} : Equivalence (fun _ _ : A => True). +Proof. + repeat constructor. +Qed. -- cgit v1.2.3