diff options
Diffstat (limited to 'lib/coq')
| -rw-r--r-- | lib/coq/Sail2_values.v | 4 |
1 files changed, 4 insertions, 0 deletions
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)). |