diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_string.v | 8 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 8 |
2 files changed, 8 insertions, 8 deletions
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v index a02556b2..0a00f8d7 100644 --- a/lib/coq/Sail2_string.v +++ b/lib/coq/Sail2_string.v @@ -7,12 +7,12 @@ Definition string_startswith s expected := let prefix := String.substring 0 (String.length expected) s in generic_eq prefix expected. -Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) := - let n := Z.to_nat (projT1 n) in +Definition string_drop s (n : Z) `{ArithFact (n >= 0)} := + let n := Z.to_nat n in String.substring n (String.length s - n) s. -Definition string_take s (n : {n : Z & ArithFact (n >= 0)}) := - let n := Z.to_nat (projT1 n) in +Definition string_take s (n : Z) `{ArithFact (n >= 0)} := + let n := Z.to_nat n in String.substring 0 n s. Definition string_length s : {n : Z & ArithFact (n >= 0)} := diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index aebc3376..37e75961 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1790,11 +1790,11 @@ match a with | None => None end. -Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) : +Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : {z : Z & ArithFact (z >= 0)} := - let z := projT1 x - projT1 y in + let z := x - 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)}) : +Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : {z : Z & ArithFact (z >= 0)} := - build_ex (Z.min (projT1 x) (projT1 y)). + build_ex (Z.min x y). |