diff options
Diffstat (limited to 'lib/coq/Sail2_string.v')
| -rw-r--r-- | lib/coq/Sail2_string.v | 8 |
1 files changed, 4 insertions, 4 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)} := |