blob: 8bd7f0a63aec4fb6047e0ff34c312b6c9b92b653 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Require Import Sail2_values.
Definition string_sub (s : string) (start : Z) (len : Z) : string :=
String.substring (Z.to_nat start) (Z.to_nat len) s.
Definition string_startswith s expected :=
let prefix := String.substring 0 (String.length expected) s in
generic_eq prefix expected.
Definition string_drop s n :=
let n := Z.to_nat n in
String.substring n (String.length s - n) s.
Definition string_length s := Z.of_nat (String.length s).
Definition string_append := String.append.
|
