From 0f2733740dd6ce6e54c576bccaede187070983ec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Jul 2016 16:09:39 +0200
Subject: [PATCH] Notation for max and min.

---
 algebra/cmra.v    | 4 ++--
 prelude/numbers.v | 2 ++
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 756af9ca3..177c51ec9 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -791,8 +791,8 @@ Section mnat.
   Instance mnat_valid : Valid mnat := λ x, True.
   Instance mnat_validN : ValidN mnat := λ n x, True.
   Instance mnat_pcore : PCore mnat := Some.
-  Instance mnat_op : Op mnat := max.
-  Definition mnat_op_max x y : x â‹… y = max x y := eq_refl.
+  Instance mnat_op : Op mnat := Nat.max.
+  Definition mnat_op_max x y : x â‹… y = x `max` y := eq_refl.
   Lemma mnat_included (x y : mnat) : x ≼ y ↔ x ≤ y.
   Proof.
     split.
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 2a410297a..0dad13378 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -32,6 +32,8 @@ Notation "(<)" := lt (only parsing) : nat_scope.
 
 Infix "`div`" := Nat.div (at level 35) : nat_scope.
 Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
+Infix "`max`" := Nat.max (at level 35) : nat_scope.
+Infix "`min`" := Nat.min (at level 35) : nat_scope.
 
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
 Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.
-- 
GitLab