diff --git a/CHANGELOG.md b/CHANGELOG.md index e3ed907a1ded2891414201b4e8a209e469e7ccbd..76e52259f4a6bd8c20c056964477e7493f848157 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -36,6 +36,7 @@ Coq 8.12 and 8.13 are no longer supported by this release. - Add `set_omap` function for finite sets and associated lemmas. (by Dorian Lesbre) - Add proof that `vec` is `Finite`. (by Herman Bergwerf.) +- Add `min` and `max` infix notations for `positive`. The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). diff --git a/stdpp/numbers.v b/stdpp/numbers.v index a33ccedff91cf1090c4292a570b4a89bffa0edcd..a9427ae880ec620b08675b95d3f0cad39a720cd9 100644 --- a/stdpp/numbers.v +++ b/stdpp/numbers.v @@ -173,6 +173,8 @@ Notation "(≤)" := Pos.le (only parsing) : positive_scope. Notation "(<)" := Pos.lt (only parsing) : positive_scope. Notation "(~0)" := xO (only parsing) : positive_scope. Notation "(~1)" := xI (only parsing) : positive_scope. +Infix "`max`" := Pos.max : positive_scope. +Infix "`min`" := Pos.min : positive_scope. Global Arguments Pos.of_nat : simpl never. Global Arguments Pos.mul : simpl never.