diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-23 16:14:43 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-23 18:20:31 -0700 |
| commit | 20bc8ab53a8a2777e54dea261b906106e7daf373 (patch) | |
| tree | 2681ab826ec78a79667ce51581b40c04a146937c /src/Util/Unit.v | |
| parent | 6335426c320d199bf821a0507b0e26d3ad67ff88 (diff) | |
Add Unit.v
Diffstat (limited to 'src/Util/Unit.v')
| -rw-r--r-- | src/Util/Unit.v | 8 |
1 files changed, 8 insertions, 0 deletions
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. |