Commit e823cff6 authored by Robbert Krebbers's avatar Robbert Krebbers

Comment about `Set_`.

parent 6f5a8ecb
...@@ -1114,7 +1114,10 @@ Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert. ...@@ -1114,7 +1114,10 @@ Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
(** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with (** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with
elements of type [A]. The first class, [SemiSet] does not include intersection elements of type [A]. The first class, [SemiSet] does not include intersection
and difference. It is useful for the case of lists, where decidable equality and difference. It is useful for the case of lists, where decidable equality
is needed to implement intersection and difference, but not union. *) is needed to implement intersection and difference, but not union.
Note that we cannot use the name [Set] since that is a reserved keyword. Hence
we use [Set_]. *)
Class SemiSet A C `{ElemOf A C, Class SemiSet A C `{ElemOf A C,
Empty C, Singleton A C, Union C} : Prop := { Empty C, Singleton A C, Union C} : Prop := {
not_elem_of_empty (x : A) : x ; not_elem_of_empty (x : A) : x ;
......
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