diff options
Diffstat (limited to 'lib/coq/Sail2_string.v')
| -rw-r--r-- | lib/coq/Sail2_string.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v index 0a63ff2c..a02556b2 100644 --- a/lib/coq/Sail2_string.v +++ b/lib/coq/Sail2_string.v @@ -11,6 +11,10 @@ Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) := let n := Z.to_nat (projT1 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 + String.substring 0 n s. + Definition string_length s : {n : Z & ArithFact (n >= 0)} := build_ex (Z.of_nat (String.length s)). |