Merge branch 'sail2' into rmem_interpreter

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)).