Commit 100c3825 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add a few comments to theories about relations.

parent 5b9c9181
(** {1 Relations} *) (** {1 Relations} *)
(** {2 Relations and orders} *)
theory EndoRelation theory EndoRelation
type t type t
...@@ -83,6 +84,8 @@ theory Inverse ...@@ -83,6 +84,8 @@ theory Inverse
predicate inv_rel (x y : t) = rel y x predicate inv_rel (x y : t) = rel y x
end end
(** {2 Closures} *)
theory ReflClosure theory ReflClosure
clone export EndoRelation clone export EndoRelation
...@@ -113,6 +116,8 @@ theory ReflTransClosure ...@@ -113,6 +116,8 @@ theory ReflTransClosure
forall x y z: t. relTR x y -> relTR y z -> relTR x z forall x y z: t. relTR x y -> relTR y z -> relTR x z
end end
(** {2 Lexicographic ordering} *)
theory Lex theory Lex
type t1 type t1
...@@ -140,6 +145,8 @@ theory MinMax ...@@ -140,6 +145,8 @@ theory MinMax
end end
*) *)
(** {2 Well-founded relation} *)
theory WellFounded theory WellFounded
type t type t
......
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