Library Poset
Module Type Poset.
Parameter set : Type.
Parameter eq : set -> set -> Prop.
Parameter eq_refl : forall x : set, eq x x.
Parameter eq_sym : forall x y : set, eq x y -> eq y x.
Parameter eq_trans : forall x y z : set, eq x y -> eq y z -> eq x z.
Parameter order : set -> set -> Prop.
Parameter order_refl : forall x y : set, eq x y -> order x y.
Parameter order_antisym : forall x y : set, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : set, order x y -> order y z -> order x z.
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans.
End Poset.
Module Type PosetSet.
Parameter set : Set.
Parameter eq : set -> set -> Prop.
Parameter eq_refl : forall x : set, eq x x.
Parameter eq_sym : forall x y : set, eq x y -> eq y x.
Parameter eq_trans : forall x y z : set, eq x y -> eq y z -> eq x z.
Parameter order : set -> set -> Prop.
Parameter order_refl : forall x y : set, eq x y -> order x y.
Parameter order_antisym : forall x y : set, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : set, order x y -> order y z -> order x z.
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans.
End PosetSet.
Index
This page has been generated by coqdoc