Skip to content
Snippets Groups Projects
Commit c6eed539 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Name some anonymous instances.

parent 260bd0b3
No related branches found
No related tags found
No related merge requests found
Pipeline #20945 passed
Stage: build
    Hide whitespace changes
    Inline Side-by-side
    theories/listset_nodup.v
    + 2
    − 2
    View file @ c6eed539
    ......@@ -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.
    ......
    0% or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment