diff options
| author | Brian Campbell | 2018-11-21 13:58:39 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-11-21 16:30:58 +0000 |
| commit | 7fbf5d8ffb99e63d46d53fc3444764986764df9f (patch) | |
| tree | cc077de42f3a8bbac01b549688b3375ce635ab3d | |
| parent | 9b68baa58c1c6a3fc28df961624c522cca74cf8c (diff) | |
Coq: min_nat
| -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)). |