Commit 34a3138e authored by Robbert Krebbers's avatar Robbert Krebbers

Move conversion functions list/option to set/disj_set to base.

parent 905a6df0
......@@ -868,6 +868,13 @@ Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level)
Notation "X ⊂ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope.
Notation "X ⊂ Y ⊂ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope.
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.
(** The class [Lexico A] is used for the lexicographic order on [A]. This order
is used to create finite maps, finite sets, etc, and is typically different from
the order [(⊆)]. *)
......
......@@ -748,13 +748,6 @@ End set.
(** * Conversion of option and list *)
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}.
Implicit Types l : list A.
......
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