mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
11 lines
132 B
Plaintext
11 lines
132 B
Plaintext
module S
|
|
|
|
use int.Int
|
|
use string.OCaml
|
|
|
|
let partial s (text: string) : ()
|
|
= let (ghost n) = length text in
|
|
assert { n >= 0 }
|
|
|
|
end
|