diff options
Diffstat (limited to 'lib/coq/Sail2_values.v')
| -rw-r--r-- | lib/coq/Sail2_values.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index c63e8453..30df0672 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1635,4 +1635,9 @@ Definition map_bind {A B} (f : A -> option B) (a : option A) : option B := match a with | Some a' => f a' | None => None -end.
\ No newline at end of file +end. + +Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) : + {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. |