From 7fbf5d8ffb99e63d46d53fc3444764986764df9f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 21 Nov 2018 13:58:39 +0000
Subject: Coq: min_nat

---
 lib/coq/Sail2_values.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 48cfc222..aebc3376 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1794,3 +1794,7 @@ Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y
   {z : Z & ArithFact (z >= 0)} :=
   let z := projT1 x - projT1 y in
   if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 0.
+
+Definition min_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+  {z : Z & ArithFact (z >= 0)} :=
+  build_ex (Z.min (projT1 x) (projT1 y)).
-- 
cgit v1.2.3