aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
diff options
context:
space:
mode:
authorReynald Affeldt2020-05-31 00:24:10 +0900
committerCyril Cohen2020-06-06 01:44:09 +0200
commit7f355343ee30f72d8ab3ce87f897dc0092e43c29 (patch)
tree3654fd4e19da8f63eecbf9a344054035a84af2eb /mathcomp/ssreflect
parentefed1800a4f2eaa942704ab8bebc60d9a3ac8dfd (diff)
tentative changelog
- mostly gathered the changes from previous commits - add `minrC` - minor doc addition to `order.v`
Diffstat (limited to 'mathcomp/ssreflect')
-rw-r--r--mathcomp/ssreflect/order.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index d8bcff1..59de10c 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -74,6 +74,8 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
(* For x, y of type T, where T is canonically a porderType d: *)
(* x <= y <-> x is less than or equal to y. *)
(* x < y <-> x is less than y (:= (y != x) && (x <= y)). *)
+(* min x y <-> if x < y then x else y *)
+(* max x y <-> if x < y then y else x *)
(* x >= y <-> x is greater than or equal to y (:= y <= x). *)
(* x > y <-> x is greater than y (:= y < x). *)
(* x <= y ?= iff C <-> x is less than y, or equal iff C is true. *)