diff options
Diffstat (limited to 'lib/coq/Sail2_string.v')
| -rw-r--r-- | lib/coq/Sail2_string.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v index 0a63ff2c..0a00f8d7 100644 --- a/lib/coq/Sail2_string.v +++ b/lib/coq/Sail2_string.v @@ -7,10 +7,14 @@ 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 : 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)} := build_ex (Z.of_nat (String.length s)). |