From c6eed5393ab7c00e766a8f5abfda5778d829ede6 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 6 Nov 2019 18:01:45 +0100 Subject: [PATCH] Name some anonymous instances. --- theories/listset_nodup.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v index 318cbaf9..59df0989 100644 --- a/theories/listset_nodup.v +++ b/theories/listset_nodup.v @@ -31,7 +31,7 @@ Instance listset_nodup_difference: Difference C := λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk), ListsetNoDup _ (NoDup_list_difference _ k Hl). -Instance: Set_ A C. +Instance listset_nodup_set: Set_ A C. Proof. split; [split | | ]. - by apply not_elem_of_nil. @@ -42,7 +42,7 @@ Proof. Qed. Global Instance listset_nodup_elems: Elements A C := listset_nodup_car. -Global Instance: FinSet A C. +Global Instance listset_nodup_fin_set: FinSet A C. Proof. split. apply _. done. by intros [??]. Qed. End list_set. -- GitLab