From 3bc164674eff753d7588c138c7f013eddbfd6e90 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 May 2019 10:23:49 +0200
Subject: [PATCH] `max` and `min` infix notations for `N` and `Z` like we have
 for `nat`.

---
 theories/numbers.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/numbers.v b/theories/numbers.v
index 7a1cfcc8..59597392 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -302,8 +302,11 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
 Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope.
 Notation "(≤)" := N.le (only parsing) : N_scope.
 Notation "(<)" := N.lt (only parsing) : N_scope.
+
 Infix "`div`" := N.div (at level 35) : N_scope.
 Infix "`mod`" := N.modulo (at level 35) : N_scope.
+Infix "`max`" := N.max (at level 35) : N_scope.
+Infix "`min`" := N.min (at level 35) : N_scope.
 
 Arguments N.add : simpl never.
 
@@ -351,6 +354,8 @@ Infix "`quot`" := Z.quot (at level 35) : Z_scope.
 Infix "`rem`" := Z.rem (at level 35) : Z_scope.
 Infix "≪" := Z.shiftl (at level 35) : Z_scope.
 Infix "≫" := Z.shiftr (at level 35) : Z_scope.
+Infix "`max`" := Z.max (at level 35) : Z_scope.
+Infix "`min`" := Z.min (at level 35) : Z_scope.
 
 Instance Zpos_inj : Inj (=) (=) Zpos.
 Proof. by injection 1. Qed.
-- 
GitLab