Commit 45ae06c7 authored by Ralf Jung's avatar Ralf Jung

add list_to_set_disj (replacing the list_to_set on gmultiset)

parent c0e1e189
Pipeline #14939 passed with stage
in 7 minutes and 35 seconds
......@@ -752,6 +752,8 @@ Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
match mx with None => | Some x => {[ x ]} end.
Fixpoint list_to_set `{Singleton A C, Empty C, Union C} (l : list A) : C :=
match l with [] => | x :: l => {[ x ]} list_to_set l end.
Fixpoint list_to_set_disj `{Singleton A C, Empty C, DisjUnion C} (l : list A) : C :=
match l with [] => | x :: l => {[ x ]} list_to_set_disj l end.
Section option_and_list_to_set.
Context `{SemiSet A C}.
......
Markdown is supported
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