mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
23 lines
645 B
Plaintext
23 lines
645 B
Plaintext
module StringCheck
|
|
|
|
use string.StringRealization as SR
|
|
|
|
clone string.String
|
|
with
|
|
function concat = SR.concat,
|
|
function length = SR.length,
|
|
predicate lt = SR.lt,
|
|
predicate le = SR.le,
|
|
function s_at = SR.s_at,
|
|
function substring = SR.substring,
|
|
predicate prefixof = SR.prefixof,
|
|
predicate suffixof = SR.suffixof,
|
|
predicate contains = SR.contains,
|
|
function indexof = SR.indexof,
|
|
function replace = SR.replace,
|
|
function replaceall = SR.replaceall,
|
|
(*predicate is_digit = SR.is_digit,*)
|
|
function to_int = SR.to_int,
|
|
function from_int = SR.from_int
|
|
|
|
end |