From c02c069326045d498a2f5f1a8f8c7beadea692c5 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.

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

diff --git a/theories/numbers.v b/theories/numbers.v
index df8c21a2..72ca465c 100644
--- a/theories/numbers.v
+++ b/theories/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